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

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