Theorem ax11indi 1360

Description: Induction step for constructing a substitution instance of ax-11o 1213 without using ax-11o 1213. 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	. . . . . . 7 |- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
2	1	ax11indn 1359	. . . . . 6 |- (-. A.x x = y -> (x = y -> (-. ph -> A.x(x = y -> -. ph))))
3	2	imp 350	. . . . 5 |- ((-. A.x x = y /\ x = y) -> (-. ph -> A.x(x = y -> -. ph)))
4		pm2.21 76	. . . . . . 7 |- (-. ph -> (ph -> ps))
5	4	imim2i 17	. . . . . 6 |- ((x = y -> -. ph) -> (x = y -> (ph -> ps)))
6	5	19.20i 989	. . . . 5 |- (A.x(x = y -> -. ph) -> A.x(x = y -> (ph -> ps)))
7	3, 6	syl6 22	. . . 4 |- ((-. A.x x = y /\ x = y) -> (-. ph -> A.x(x = y -> (ph -> ps))))
8		ax11indi.2	. . . . . 6 |- (-. A.x x = y -> (x = y -> (ps -> A.x(x = y -> ps))))
9	8	imp 350	. . . . 5 |- ((-. A.x x = y /\ x = y) -> (ps -> A.x(x = y -> ps)))
10		ax-1 4	. . . . . . 7 |- (ps -> (ph -> ps))
11	10	imim2i 17	. . . . . 6 |- ((x = y -> ps) -> (x = y -> (ph -> ps)))
12	11	19.20i 989	. . . . 5 |- (A.x(x = y -> ps) -> A.x(x = y -> (ph -> ps)))
13	9, 12	syl6 22	. . . 4 |- ((-. A.x x = y /\ x = y) -> (ps -> A.x(x = y -> (ph -> ps))))
14	7, 13	jaod 424	. . 3 |- ((-. A.x x = y /\ x = y) -> ((-. ph \/ ps) -> A.x(x = y -> (ph -> ps))))
15		imor 234	. . 3 |- ((ph -> ps) <-> (-. ph \/ ps))
16	14, 15	syl5ib 206	. 2 |- ((-. A.x x = y /\ x = y) -> ((ph -> ps) -> A.x(x = y -> (ph -> ps))))
17	16	ex 373	1 |- (-. A.x x = y -> (x = y -> ((ph -> ps) -> A.x(x = y -> (ph -> ps)))))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223  A.wal 951   = wceq 953

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978

Copyright terms: Public domain