Proof of proveit.logic.booleans.quantification.universality.forall_with_conditions__is_bool theorem

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit import Conditional
from proveit.core_expr_types import P__x_1_to_n, Q__x_1_to_n
from proveit.logic.booleans.quantification.universality  import forall_in_bool

%proving forall_with_conditions__is_bool

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
forall_with_conditions__is_bool:
(see dependencies)

forall_with_conditions__is_bool may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

defaults.assumptions = forall_with_conditions__is_bool.conditions

defaults.assumptions:

forall_in_bool

 ⊢  

forall_in_bool.instantiate({P__x_1_to_n: Conditional(P__x_1_to_n, Q__x_1_to_n)})

 ⊢  

%qed

proveit.logic.booleans.quantification.universality.forall_with_conditions__is_bool has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 8, 3	⊢
	: , :
2	axiom		⊢
	proveit.logic.booleans.quantification.universality.forall_in_bool
3	instantiation	4, 5	⊢
	: , :
4	conjecture		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
5	instantiation	6, 7, 8	⊢
	: , : , :
6	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
7	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
8	assumption		⊢