Theorem ax11indi 2196

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

Hypotheses

Ref	Expression
ax11indn.1	|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
ax11indi.2	|- (-. A.x x = y -> (x = y -> (ps -> A.x(x = y -> ps))))

Assertion

Ref	Expression
ax11indi	|- (-. A.x x = y -> (x = y -> ((ph -> ps) -> A.x(x = y -> (ph -> ps)))))

Proof of Theorem ax11indi

Step	Hyp	Ref	Expression
1		ax11indn.1	. . . . . 6 |- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
2	1	ax11indn 2195	. . . . 5 |- (-. A.x x = y -> (x = y -> (-. ph -> A.x(x = y -> -. ph))))
3	2	imp 418	. . . 4 |- ((-. A.x x = y /\ x = y) -> (-. ph -> A.x(x = y -> -. ph)))
4		pm2.21 100	. . . . . 6 |- (-. ph -> (ph -> ps))
5	4	imim2i 13	. . . . 5 |- ((x = y -> -. ph) -> (x = y -> (ph -> ps)))
6	5	alimi 1559	. . . 4 |- (A.x(x = y -> -. ph) -> A.x(x = y -> (ph -> ps)))
7	3, 6	syl6 29	. . 3 |- ((-. A.x x = y /\ x = y) -> (-. ph -> A.x(x = y -> (ph -> ps))))
8		ax11indi.2	. . . . 5 |- (-. A.x x = y -> (x = y -> (ps -> A.x(x = y -> ps))))
9	8	imp 418	. . . 4 |- ((-. A.x x = y /\ x = y) -> (ps -> A.x(x = y -> ps)))
10		ax-1 6	. . . . . 6 |- (ps -> (ph -> ps))
11	10	imim2i 13	. . . . 5 |- ((x = y -> ps) -> (x = y -> (ph -> ps)))
12	11	alimi 1559	. . . 4 |- (A.x(x = y -> ps) -> A.x(x = y -> (ph -> ps)))
13	9, 12	syl6 29	. . 3 |- ((-. A.x x = y /\ x = y) -> (ps -> A.x(x = y -> (ph -> ps))))
14	7, 13	jad 154	. 2 |- ((-. A.x x = y /\ x = y) -> ((ph -> ps) -> A.x(x = y -> (ph -> ps))))
15	14	ex 423	1 |- (-. A.x x = y -> (x = y -> ((ph -> ps) -> A.x(x = y -> (ph -> ps)))))

Syntax hints:  -. wn 3   -> wi 4   /\ wa 358  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542

This theorem is referenced by: (None)