Theorem Dependencies

proveit.logic.booleans.in_bool_if_true

see proof

import proveit
# Automation is not needed when querying dependencies:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
from proveit.logic.booleans import in_bool_if_true

%dependencies in_bool_if_true

Unproven conjectures required (directly or indirectly) to prove in_bool_if_true

proveit.numbers.numerals.decimals.add_1_1

Axioms required (directly or indirectly) to prove in_bool_if_true

proveit.logic.booleans.disjunction.or_t_f

proveit.logic.booleans.eq_true_elim

proveit.logic.booleans.eq_true_intro

proveit.logic.booleans.false_not_true

proveit.logic.booleans.negation.negation_elim

proveit.logic.equality.equals_reflexivity

proveit.logic.equality.equals_symmetry

proveit.logic.equality.equals_transitivity

proveit.logic.equality.not_equals_def

proveit.logic.equality.substitution

proveit.logic.sets.enumeration.enum_set_def

proveit.numbers.number_sets.natural_numbers.successor_in_nats

proveit.numbers.number_sets.natural_numbers.zero_in_nats

proveit.numbers.numerals.decimals.one_def

Conservative definitions used (but not logically required) to prove in_bool_if_true

proveit.logic.booleans.bools_def

proveit.numbers.numerals.decimals.tuple_len_2_typical_eq

Theorems/conjectures that depend directly on in_bool_if_true

proveit.logic.booleans.conjunction.binary_closure

proveit.logic.booleans.conjunction.falsified_and_if_not_left

proveit.logic.booleans.conjunction.falsified_and_if_not_right

proveit.logic.booleans.disjunction.binary_closure

proveit.logic.booleans.disjunction.demorgans_law_and_to_or_bin

proveit.logic.booleans.disjunction.not_left_if_neither

proveit.logic.booleans.disjunction.not_right_if_neither

proveit.logic.booleans.false_is_bool

proveit.logic.booleans.forall_over_bool_by_cases

proveit.logic.booleans.implication.iff_closure

proveit.logic.booleans.implication.implication_closure

proveit.logic.booleans.in_bool_if_false

proveit.logic.booleans.negation.double_negation_elim

proveit.logic.booleans.unfold_is_bool

proveit.logic.sets.set_subset_eq_of_union_with_set

proveit.numbers.ordering.max_bin_args_commute

proveit.numbers.ordering.max_y_ge_x

proveit.numbers.ordering.min_bin_args_commute

proveit.numbers.ordering.min_nat_n_zero_is_zero

proveit.numbers.ordering.min_y_le_x

proveit.numbers.ordering.transitivity_less_eq_less

proveit.numbers.ordering.transitivity_less_eq_less_eq

proveit.numbers.ordering.transitivity_less_less_eq

proveit.physics.quantum.QPE._best_guarantee_delta_nonzero

proveit.physics.quantum.QPE._fail_sum_prob_conds_equiv_lemma

proveit.physics.quantum.QPE._scaled_delta_b_not_eq_nonzeroInt