Theorem ax11indi 1758

Description: Induction step for constructing a substitution instance of ax-11o 1588 without using ax-11o 1588. Implication case.

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 1757	. . . . 5 |- (-. A.x x = y -> (x = y -> (-. ph -> A.x(x = y -> -. ph))))
3	2	imp 377	. . . 4 |- ((-. A.x x = y /\ x = y) -> (-. ph -> A.x(x = y -> -. ph)))
4		pm2.21 92	. . . . . 6 |- (-. ph -> (ph -> ps))
5	4	imim2i 11	. . . . 5 |- ((x = y -> -. ph) -> (x = y -> (ph -> ps)))
6	5	alimi 1338	. . . 4 |- (A.x(x = y -> -. ph) -> A.x(x = y -> (ph -> ps)))
7	3, 6	syl6 25	. . 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 377	. . . 4 |- ((-. A.x x = y /\ x = y) -> (ps -> A.x(x = y -> ps)))
10		ax-1 4	. . . . . 6 |- (ps -> (ph -> ps))
11	10	imim2i 11	. . . . 5 |- ((x = y -> ps) -> (x = y -> (ph -> ps)))
12	11	alimi 1338	. . . 4 |- (A.x(x = y -> ps) -> A.x(x = y -> (ph -> ps)))
13	9, 12	syl6 25	. . 3 |- ((-. A.x x = y /\ x = y) -> (ps -> A.x(x = y -> (ph -> ps))))
14	7, 13	jad 156	. 2 |- ((-. A.x x = y /\ x = y) -> ((ph -> ps) -> A.x(x = y -> (ph -> ps))))
15	14	ex 402	1 |- (-. A.x x = y -> (x = y -> ((ph -> ps) -> A.x(x = y -> (ph -> ps)))))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain