Theorem a5i 965

Description: Inference from ax-5 952.

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

Syntax hints:   -> wi 3  A.wal 950

This theorem is referenced by:  19.20i 968  hba1 979  hbae 1128  equs4 1133  equsal 1134  hbs1f 1172  hbsb2a 1187  hbsb2e 1188  aev 1192  hbsb2 1211  ax11indalem 1345  ax11inda2ALT 1346  a12studyALT 1356  exists2 1435  reu3 1902  sbcralt 1961  sbcralgf 1963  axunndlem1 4870  axregnd 4879  axacndlem3 4884  axacndlem5 4886  axacnd 4887

This theorem was proved from axioms:  ax-mp 7  ax-5 952  ax-gen 955

Copyright terms: Public domain