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

Theorem alrimih 1575
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 1569 . 2  |-  ( A. x ph  ->  A. x ps )
41, 3syl 16 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550
This theorem is referenced by:  eximdh  1599  nexdh  1600  albidh  1601  exbidh  1602  alrimiv  1642  ax11i  1658  cbvaliw  1686  alrimi  1782  hbnOLD  1803  hbimdOLD  1836  hbimOLD  1838  19.23hOLD  1840  spimehOLD  1841  equsalhwOLD  1862  19.21hOLD  1863  19.12OLD  1871  cbv3hvOLD  1880  hbnd  1906  dvelimvOLD  2029  aev  2048  a16gOLD  2050  a5i-o  2229  equidq  2254  aev-o  2261  ax11f  2271  eujustALT  2286  axi5r  2411  ceqsex3OLD  26711  ax4567  27580  hbimpg  28703  gen11nv  28780  bnj1093  29411  cbv3hvNEW7  29508  19.12vAUX7  29516  dvelimvNEW7  29524  hbaew2AUX7  29541  aevwAUX7  29584  a16gNEW7  29608  ax7w4AUX7  29720  19.12OLD7  29748
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1556  ax-5 1567
  Copyright terms: Public domain W3C validator