Metamath Proof Explorer


Theorem ax12indi

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Implication case. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ax12indn.1 ¬ x x = y x = y φ x x = y φ
ax12indi.2 ¬ x x = y x = y ψ x x = y ψ
Assertion ax12indi ¬ x x = y x = y φ ψ x x = y φ ψ

Proof

Step Hyp Ref Expression
1 ax12indn.1 ¬ x x = y x = y φ x x = y φ
2 ax12indi.2 ¬ x x = y x = y ψ x x = y ψ
3 1 ax12indn ¬ x x = y x = y ¬ φ x x = y ¬ φ
4 3 imp ¬ x x = y x = y ¬ φ x x = y ¬ φ
5 pm2.21 ¬ φ φ ψ
6 5 imim2i x = y ¬ φ x = y φ ψ
7 6 alimi x x = y ¬ φ x x = y φ ψ
8 4 7 syl6 ¬ x x = y x = y ¬ φ x x = y φ ψ
9 2 imp ¬ x x = y x = y ψ x x = y ψ
10 ax-1 ψ φ ψ
11 10 imim2i x = y ψ x = y φ ψ
12 11 alimi x x = y ψ x x = y φ ψ
13 9 12 syl6 ¬ x x = y x = y ψ x x = y φ ψ
14 8 13 jad ¬ x x = y x = y φ ψ x x = y φ ψ
15 14 ex ¬ x x = y x = y φ ψ x x = y φ ψ