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

Theorem alrimih 1553
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 1546 . 2  |-  ( A. x ph  ->  A. x ps )
41, 3syl 17 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532
This theorem is referenced by:  eximdh  1586  nexdh  1588  albidh  1589  exbidh  1590  ax12o10lem3  1637  ax12o10lem6  1640  ax12o10lem7  1641  ax12o10lem8  1642  ax12o10lem11  1645  ax12o10lem14  1648  ax12olem16  1650  ax12olem17  1651  ax12olem20  1654  ax10lem19  1668  ax10lem24  1673  a16gALT  1679  ax9  1683  equidq  1689  alrimi  1706  hbim  1723  hbnd  1808  hbim1  1810  equid  1818  ax11i  1833  equsalh  1852  aev-o  1925  ax11f  2110  eujustALT  2120  ceqsex3OLD  26058  ax4567  26933  hbimpg  27336  gen11nv  27402  bnj1093  28022  ax12o10lem3X  28164  ax12o10lem3K  28165  ax12o10lem6K  28170  ax12o10lem6X  28171  ax12o10lem7K  28172  ax12o10lem7X  28173  ax12o10lem8K  28174  ax12o10lem8X  28175  ax12o10lem11K  28180  ax12o10lem11X  28181  ax12o10lem14K  28186  ax12o10lem14X  28187  ax12olem16K  28191  ax12olem16X  28192  ax12olem17K  28193  ax12olem17X  28194  ax12olem20K  28199  ax12olem20X  28200  ax10lem19X  28218  ax10lem24X  28223  a16gALTX  28228  ax9X  28232  hbae-x12  28239  ax10lem17ALT  28253  ax9lem3  28272  ax9lem6  28275  ax9lem8  28277  ax9lem9  28278  ax9lem10  28279  ax9lem12  28281  ax9lem13  28282  ax9lem17  28286  ax9vax9  28288
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10  ax-5 1533  ax-gen 1536
  Copyright terms: Public domain W3C validator