Theorem axc4i 1920

Description: Inference version of axc4 1878. (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 1919	. 2 |- F/ x A. x ph
2		axc4i.1	. 2 |- ( A. x ph -> ps )
3	1, 2	alrimi 1895	1 |- ( A. x ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-12 1872

This theorem depends on definitions:  df-bi 185  df-ex 1628  df-nf 1632

This theorem is referenced by:  hbae  2075  hbsb2  2117  hbsb2a  2119  hbsb2e  2120  reu6  3230  axunndlem1  8905  axregndOLD  8915  axacndlem3  8920  axacndlem5  8922  axacnd  8923  pm11.57  31503  pm11.59  31505  axc5c4c711toc7  31519  axc11next  31521  hbalg  33707  ax6e2eq  33709  ax6e2eqVD  34093  bj-nfs1t  34660  bj-hbsb2v  34725  bj-hbsb2av  34727  bj-hbaeb2  34777  frege93  38494