# Proof of proveit.logic.booleans.conjunction.and_if_both theorem¶

In [1]:
import proveit
from proveit import A, B
from proveit.logic.booleans.conjunction import true_and_true
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving and_if_both

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
and_if_both:
(see dependencies)
and_if_both may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [3]:
AeqT = A.evaluation(assumptions=[A])

AeqT:
In [4]:
BeqT = B.evaluation(assumptions=[B])

BeqT:
In [5]:
true_and_true

In [6]:
AandT = AeqT.sub_left_side_into(true_and_true.inner_expr().operands[0],
auto_simplify=False)

AandT:
In [7]:
AandB = BeqT.sub_left_side_into(AandT, assumptions=[A, B],
auto_simplify=False)

AandB: ,  ⊢
In [8]:
# To do this manually, execute AandB.generalize((A, B), conditions=[A, B]).
# But this can be figured out via automation.
%qed

proveit.logic.booleans.conjunction.and_if_both has been proven.

Out[8]:
step typerequirementsstatement
0generalization1
1instantiation4, 2, 3,  ⊢
: , :
2instantiation4, 5, 6
: , :
3assumption
4theorem
proveit.logic.equality.substitute_truth
5theorem
proveit.logic.booleans.conjunction.true_and_true
6assumption