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 ) ) ) )