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

Theorem alrimih 1574
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 1568 . 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 1549
This theorem is referenced by:  eximdh  1598  nexdh  1599  albidh  1600  exbidh  1601  alrimiv  1641  ax11i  1657  cbvaliw  1685  alrimi  1781  hbnOLD  1802  hbimdOLD  1835  hbimOLD  1837  19.23hOLD  1839  spimehOLD  1840  equsalhwOLD  1861  19.21hOLD  1862  19.12OLD  1870  cbv3hvOLD  1879  hbnd  1905  dvelimvOLD  2028  aev  2047  a16gOLD  2049  a5i-o  2226  equidq  2251  aev-o  2258  ax11f  2268  eujustALT  2283  axi5r  2402  ceqsex3OLD  26641  ax4567  27511  hbimpg  28394  gen11nv  28470  bnj1093  29101  cbv3hvNEW7  29198  19.12vAUX7  29206  dvelimvNEW7  29214  hbaew2AUX7  29231  aevwAUX7  29272  a16gNEW7  29296  ax7w4AUX7  29404  19.12OLD7  29416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1555  ax-5 1566
  Copyright terms: Public domain W3C validator