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

Theorem a5i 1807
Description: Inference version of ax5o 1765. (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 1806 . 2  |-  F/ x A. x ph
2 a5i.1 . 2  |-  ( A. x ph  ->  ps )
31, 2alrimi 1781 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549
This theorem is referenced by:  hbae  2040  hbaeOLD  2041  hbsb2  2091  hbsb2a  2093  hbsb2e  2094  reu6  3116  axunndlem1  8463  axregnd  8472  axacndlem3  8477  axacndlem5  8479  axacnd  8480  pm11.57  27557  pm11.59  27559  ax4567to6  27573  ax10ext  27575  hbalg  28580  a9e2eq  28582  a9e2eqVD  28957  hba1eAUX7  29415  hbaewAUX7  29416  hbsb2aNEW7  29480  hbsb2eNEW7  29481  hbsb2NEW7  29492  hbaew4AUX7  29586  ax7w3AUX7  29589  ax7w9AUX7  29598  ax7w16AUX7  29612  hbaeOLD7  29646
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator