Theorem a5i 988

Description: Inference from ax-5o 974.

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 974	. 2 |- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
2		a5i.1	. 2 |- (A.xph -> ps)
3	1, 2	mpg 985	1 |- (A.xph -> A.xps)

Syntax hints:   -> wi 3  A.wal 953

This theorem is referenced by:  19.20i 991  hba1 1002  hbae 1144  equs4 1149  equsal 1150  hbs1f 1189  hbsb2a 1204  hbsb2e 1205  aev 1208  hbsb2 1227  ax11indalem 1368  ax11inda2ALT 1369  a12studyALT 1379  exists2 1458  reu3 1929  sbcralt 1988  sbcralgf 1990  axunndlem1 4934  axregnd 4943  axacndlem3 4948  axacndlem5 4950  axacnd 4951

This theorem was proved from axioms:  ax-mp 7  ax-gen 962  ax-5o 974

Copyright terms: Public domain