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

Theorem alrimih 1565
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
alrimih.1  |-  ( ph  ->  A. x ph )
alrimih.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
alrimih  |-  ( ph  ->  A. x ps )

Proof of Theorem alrimih
StepHypRef Expression
1 alrimih.1 . 2  |-  ( ph  ->  A. x ph )
2 alrimih.2 . . 3  |-  ( ph  ->  ps )
32alimi 1559 . 2  |-  ( A. x ph  ->  A. x ps )
41, 3syl 15 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1540
This theorem is referenced by:  eximdh  1588  nexdh  1589  albidh  1590  exbidh  1591  alrimiv  1631  ax11i  1647  cbvaliw  1673  alrimi  1766  hbnOLD  1778  hbimdOLD  1818  hbimOLD  1820  19.23hOLD  1822  spimehOLD  1823  equsalhwOLD  1844  19.21hOLD  1845  19.12OLD  1853  cbv3hvOLD  1856  hbnd  1887  dvelimv  1944  a16g  1950  aev  1996  a5i-o  2155  equidq  2180  aev-o  2187  ax11f  2197  eujustALT  2212  ceqsex3OLD  26049  ax4567  26924  hbimpg  28048  gen11nv  28123  bnj1093  28755  cbv3hvNEW7  28852  19.12vAUX7  28860  dvelimvNEW7  28868  hbaew2AUX7  28885  aevwAUX7  28926  a16gNEW7  28950  ax7w4AUX7  29058  19.12OLD7  29070  hbae-x12  29161  ax10lem17ALT  29175  ax9lem3  29194  ax9lem6  29197  ax9lem8  29199  ax9lem9  29200  ax9lem10  29201  ax9lem12  29203  ax9lem13  29204  ax9lem17  29208  ax9vax9  29210
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1546  ax-5 1557
  Copyright terms: Public domain W3C validator