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

Theorem a5i 1770
Description: Inference version of ax5o 1729. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
a5i.1  |-  ( A. x ph  ->  ps )
Assertion
Ref Expression
a5i  |-  ( A. x ph  ->  A. x ps )

Proof of Theorem a5i
StepHypRef Expression
1 nfa1 1768 . 2  |-  F/ x A. x ph
2 a5i.1 . 2  |-  ( A. x ph  ->  ps )
31, 2alrimi 1757 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  hbae  1906  hbsb2a  1994  hbsb2e  1995  hbsb2  2010  reu6  2967  axunndlem1  8233  axregnd  8242  axacndlem3  8247  axacndlem5  8249  axacnd  8250  pm11.57  27691  pm11.59  27693  ax4567to6  27707  ax10ext  27709  hbalg  28620  a9e2eq  28622  a9e2eqVD  28999  hba1eAUX7  29454  hbaewAUX7  29455  hbsb2aNEW7  29517  hbsb2eNEW7  29518  hbsb2NEW7  29529  hbaew4AUX7  29618  ax7w9AUX7  29630  hbaeOLD7  29662  a12studyALT  29755  a12study3  29757
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator