Theorem axc4i 1837

Description: Inference version of axc4 1800. (Contributed by NM, 3-Jan-1993.)

Hypothesis

Ref	Expression
axc4i.1	|- ( A. x ph -> ps )

Assertion

Ref	Expression
axc4i	|- ( A. x ph -> A. x ps )

Proof of Theorem axc4i

Step	Hyp	Ref	Expression
1		nfa1 1836	. 2 |- F/ x A. x ph
2		axc4i.1	. 2 |- ( A. x ph -> ps )
3	1, 2	alrimi 1816	1 |- ( A. x ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591

This theorem is referenced by:  hbae  2015  hbsb2  2059  hbsb2a  2061  hbsb2e  2062  reu6  3255  axunndlem1  8873  axregndOLD  8885  axacndlem3  8890  axacndlem5  8892  axacnd  8893  pm11.57  29810  pm11.59  29812  axc5c4c711toc7  29826  axc11next  29828  hbalg  31616  ax6e2eq  31618  ax6e2eqVD  31995  bj-nfs1t  32562  bj-hbsb2v  32626  bj-hbsb2av  32628