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

Theorem alrimih 1571
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 1565 . 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 1546
This theorem is referenced by:  eximdh  1595  nexdh  1596  albidh  1597  exbidh  1598  alrimiv  1638  ax11i  1654  cbvaliw  1681  alrimi  1777  hbnOLD  1798  hbimdOLD  1831  hbimOLD  1833  19.23hOLD  1835  spimehOLD  1836  equsalhwOLD  1857  19.21hOLD  1858  19.12OLD  1866  cbv3hvOLD  1875  hbnd  1901  dvelimvOLD  1994  aev  2011  a16gOLD  2013  a5i-o  2200  equidq  2225  aev-o  2232  ax11f  2242  eujustALT  2257  axi5r  2376  ceqsex3OLD  26599  ax4567  27469  hbimpg  28352  gen11nv  28427  bnj1093  29055  cbv3hvNEW7  29152  19.12vAUX7  29160  dvelimvNEW7  29168  hbaew2AUX7  29185  aevwAUX7  29226  a16gNEW7  29250  ax7w4AUX7  29358  19.12OLD7  29370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1552  ax-5 1563
  Copyright terms: Public domain W3C validator