MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axc4i Structured version   Unicode version

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
StepHypRef Expression
1 nfa1 1919 . 2  |-  F/ x A. x ph
2 axc4i.1 . 2  |-  ( A. x ph  ->  ps )
31, 2alrimi 1895 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator