Theorem Dependencies

proveit.logic.equality.lhs_via_equality

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.equality import lhs_via_equality

%dependencies lhs_via_equality

Axioms required (directly or indirectly) to prove lhs_via_equality

proveit.logic.booleans.eq_true_elim

proveit.logic.booleans.eq_true_intro

proveit.logic.equality.equals_transitivity

proveit.logic.equality.substitution

Theorems/conjectures that depend directly on lhs_via_equality

proveit.core_expr_types.tuples.tuple_eq_via_elem_eq

proveit.logic.booleans.implication.iff_intro

proveit.logic.equality.equals_reversal

proveit.logic.equality.sub_in_left_operands

proveit.logic.equality.sub_in_left_operands_via_tuple

proveit.logic.sets.enumeration.fold

proveit.logic.sets.equivalence.fold_set_not_equiv

proveit.logic.sets.equivalence.set_equiv_fold

proveit.logic.sets.inclusion.fold_not_proper_subset

proveit.logic.sets.inclusion.fold_not_subset_eq

proveit.logic.sets.inclusion.fold_proper_subset

proveit.logic.sets.inclusion.fold_subset_eq

proveit.logic.sets.inclusion.transitivity_subset_eq_subset_eq

proveit.logic.sets.intersection_is_subset_eq

proveit.logic.sets.intersection_subset_eq_union

proveit.logic.sets.membership.fold_not_in_set

proveit.logic.sets.set_subset_eq_of_union_with_set