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

Metamath Proof Explorer

Theorem ax12inda2

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Quantification case. When z and y are distinct, this theorem avoids the dummy variables needed by the more general ax12inda . (Contributed by NM, 24-Jan-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 ax12inda2 
|- ( -. 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. z ph -> ( x = y -> A. z ph ) )
3 axc16g-o 
 |-  ( A. y y = z -> ( ( x = y -> A. z ph ) -> A. x ( x = y -> A. z ph ) ) )
4 2 3 syl5 
 |-  ( A. y y = z -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
5 4 a1d 
 |-  ( A. y y = z -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )
6 5 a1d 
 |-  ( A. y y = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
7 1 ax12indalem 
 |-  ( -. A. y y = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
8 6 7 pm2.61i 
 |-  ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )