Theorem a5i 989

Description: Inference from ax-5o 975.

Hypothesis

Ref	Expression
a5i.1	|- (A.xph -> ps)

Assertion

Ref	Expression
a5i	|- (A.xph -> A.xps)

Proof of Theorem a5i

Step	Hyp	Ref	Expression
1		ax-5o 975	. 2 |- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
2		a5i.1	. 2 |- (A.xph -> ps)
3	1, 2	mpg 986	1 |- (A.xph -> A.xps)

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  19.20i 992  hba1 1003  hbae 1145  equs4 1150  equsal 1151  hbs1f 1189  hbsb2a 1204  hbsb2e 1205  aev 1208  hbsb2 1227  ax11indalem 1368  ax11inda2ALT 1369  a12studyALT 1379  exists2 1458  reu3 1931  sbcralt 1990  sbcralgf 1992  axunndlem1 4947  axregnd 4956  axacndlem3 4961  axacndlem5 4963  axacnd 4964

This theorem was proved from axioms:  ax-mp 7  ax-gen 963  ax-5o 975

Copyright terms: Public domain