Theorem ax5 1160

Description: Rederivation of axiom ax-5 1140 from the orginal version, ax-5o 1159. See ax5o 1158 for the derivation of ax-5o 1159 from ax-5 1140.

This theorem should not be referenced in any proof. Instead, use ax-5 1140 above so that uses of ax-5 1140 can be more easily identified.

Note: This is the same as theorem alim 1178 below. It is proved separately here so that it won't be dependent on the axioms used for alim 1178 (which may change in the future).

Assertion

Ref	Expression
ax5	|- (A.x(ph -> ps) -> (A.xph -> A.xps))

Proof of Theorem ax5

Step	Hyp	Ref	Expression
1		ax-4 1157	. . . . 5 |- (A.x(ph -> ps) -> (ph -> ps))
2		ax-4 1157	. . . . 5 |- (A.xph -> ph)
3	1, 2	syl5 20	. . . 4 |- (A.x(ph -> ps) -> (A.xph -> ps))
4	3	ax-gen 1143	. . 3 |- A.x(A.x(ph -> ps) -> (A.xph -> ps))
5		ax-5o 1159	. . 3 |- (A.x(A.x(ph -> ps) -> (A.xph -> ps)) -> (A.x(ph -> ps) -> A.x(A.xph -> ps)))
6	4, 5	ax-mp 7	. 2 |- (A.x(ph -> ps) -> A.x(A.xph -> ps))
7		ax-5o 1159	. 2 |- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
8	6, 7	syl 12	1 |- (A.x(ph -> ps) -> (A.xph -> A.xps))

Syntax hints:   -> wi 3  A.wal 1134

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 1143  ax-4 1157  ax-5o 1159

Copyright terms: Public domain