# Proof of proveit.logic.equality.sub_left_side_into theorem¶

In [1]:
import proveit
from proveit import defaults
from proveit import f, x, y, P, Px, Py
from proveit.logic import Equals
from proveit.logic.equality  import substitution
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving sub_left_side_into

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
sub_left_side_into:
(see dependencies)
In [3]:
defaults.assumptions = sub_left_side_into.all_conditions()

defaults.assumptions:
In [4]:
substitution

In [5]:
# P(x)=P(y) from x=y via substitution
substitution.instantiate({f:P, x:x, y:y})

In [6]:
Py.prove().evaluation()

In [7]:
# P(x)=TRUE via P(y)=TRUE and transitivity
Px.evaluation()

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

In [8]:
%qed

proveit.logic.equality.sub_left_side_into has been proven.

Out[8]:
step typerequirementsstatement
0generalization1
1instantiation2, 3,  ⊢
:
2axiom
proveit.logic.booleans.eq_true_elim
3instantiation4, 5, 6,  ⊢
: , : , :
4axiom
proveit.logic.equality.equals_transitivity
5instantiation7, 8
: , : , :
6instantiation9, 10
:
7axiom
proveit.logic.equality.substitution
8assumption
9axiom
proveit.logic.booleans.eq_true_intro
10assumption