Theorem a5i 1030

Description: Inference from ax-5o 1016.

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

Syntax hints:   -> wi 3  A.wal 995

This theorem is referenced by:  19.20i 1033  hba1 1044  hbae 1187  equs4 1192  equsal 1193  hbs1f 1231  hbsb2a 1246  hbsb2e 1247  aev 1250  hbsb2 1269  ax11indalem 1410  ax11inda2ALT 1411  a12studyALT 1421  exists2 1503  reu3 1978  sbcralt 2040  sbcralgf 2042  axunndlem1 5012  axregnd 5021  axacndlem3 5026  axacndlem5 5028  axacnd 5029

This theorem was proved from axioms:  ax-mp 7  ax-gen 1004  ax-5o 1016

Copyright terms: Public domain