This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax12inda2ALT

Description: Alternate proof of ax12inda2 , slightly more direct and not requiring ax-c16 . (Contributed by NM, 4-May-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12inda2.1 
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Assertion ax12inda2ALT 
|- ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )

Proof

Step Hyp Ref Expression
1 ax12inda2.1 
 |-  ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
2 ax-1 
 |-  ( A. x ph -> ( x = y -> A. x ph ) )
3 2 axc4i-o 
 |-  ( A. x ph -> A. x ( x = y -> A. x ph ) )
4 3 a1i 
 |-  ( A. z z = x -> ( A. x ph -> A. x ( x = y -> A. x ph ) ) )
5 biidd 
 |-  ( A. z z = x -> ( ph <-> ph ) )
6 5 dral1-o 
 |-  ( A. z z = x -> ( A. z ph <-> A. x ph ) )
7 6 imbi2d 
 |-  ( A. z z = x -> ( ( x = y -> A. z ph ) <-> ( x = y -> A. x ph ) ) )
8 7 dral2-o 
 |-  ( A. z z = x -> ( A. x ( x = y -> A. z ph ) <-> A. x ( x = y -> A. x ph ) ) )
9 4 6 8 3imtr4d 
 |-  ( A. z z = x -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
10 9 aecoms-o 
 |-  ( A. x x = z -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
11 10 a1d 
 |-  ( A. x x = z -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )
12 11 a1d 
 |-  ( A. x x = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
13 simplr 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> -. A. x x = y )
14 dveeq1-o 
 |-  ( -. A. z z = x -> ( x = y -> A. z x = y ) )
15 14 naecoms-o 
 |-  ( -. A. x x = z -> ( x = y -> A. z x = y ) )
16 15 imp 
 |-  ( ( -. A. x x = z /\ x = y ) -> A. z x = y )
17 16 adantlr 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> A. z x = y )
18 hbnae-o 
 |-  ( -. A. x x = y -> A. z -. A. x x = y )
19 hba1-o 
 |-  ( A. z x = y -> A. z A. z x = y )
20 18 19 hban 
 |-  ( ( -. A. x x = y /\ A. z x = y ) -> A. z ( -. A. x x = y /\ A. z x = y ) )
21 ax-c5 
 |-  ( A. z x = y -> x = y )
22 1 imp 
 |-  ( ( -. A. x x = y /\ x = y ) -> ( ph -> A. x ( x = y -> ph ) ) )
23 21 22 sylan2 
 |-  ( ( -. A. x x = y /\ A. z x = y ) -> ( ph -> A. x ( x = y -> ph ) ) )
24 20 23 alimdh 
 |-  ( ( -. A. x x = y /\ A. z x = y ) -> ( A. z ph -> A. z A. x ( x = y -> ph ) ) )
25 13 17 24 syl2anc 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> ( A. z ph -> A. z A. x ( x = y -> ph ) ) )
26 ax-11 
 |-  ( A. z A. x ( x = y -> ph ) -> A. x A. z ( x = y -> ph ) )
27 hbnae-o 
 |-  ( -. A. x x = z -> A. x -. A. x x = z )
28 hbnae-o 
 |-  ( -. A. x x = z -> A. z -. A. x x = z )
29 28 15 nf5dh 
 |-  ( -. A. x x = z -> F/ z x = y )
30 19.21t 
 |-  ( F/ z x = y -> ( A. z ( x = y -> ph ) <-> ( x = y -> A. z ph ) ) )
31 29 30 syl 
 |-  ( -. A. x x = z -> ( A. z ( x = y -> ph ) <-> ( x = y -> A. z ph ) ) )
32 27 31 albidh 
 |-  ( -. A. x x = z -> ( A. x A. z ( x = y -> ph ) <-> A. x ( x = y -> A. z ph ) ) )
33 26 32 imbitrid 
 |-  ( -. A. x x = z -> ( A. z A. x ( x = y -> ph ) -> A. x ( x = y -> A. z ph ) ) )
34 33 ad2antrr 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> ( A. z A. x ( x = y -> ph ) -> A. x ( x = y -> A. z ph ) ) )
35 25 34 syld 
 |-  ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
36 35 exp31 
 |-  ( -. A. x x = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
37 12 36 pm2.61i 
 |-  ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )