Metamath Proof Explorer


Theorem ax12indn

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

Ref Expression
Hypothesis ax12indn.1 ¬ x x = y x = y φ x x = y φ
Assertion ax12indn ¬ 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 19.8a x = y ¬ φ x x = y ¬ φ
3 exanali x x = y ¬ φ ¬ x x = y φ
4 hbn1 ¬ x x = y x ¬ x x = y
5 hbn1 ¬ x x = y φ x ¬ x x = y φ
6 con3 φ x x = y φ ¬ x x = y φ ¬ φ
7 1 6 syl6 ¬ x x = y x = y ¬ x x = y φ ¬ φ
8 7 com23 ¬ x x = y ¬ x x = y φ x = y ¬ φ
9 4 5 8 alrimdh ¬ x x = y ¬ x x = y φ x x = y ¬ φ
10 3 9 syl5bi ¬ x x = y x x = y ¬ φ x x = y ¬ φ
11 2 10 syl5 ¬ x x = y x = y ¬ φ x x = y ¬ φ
12 11 expd ¬ x x = y x = y ¬ φ x x = y ¬ φ