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  2111  eujustALT  2121  ceqsex3OLD  26093  ax4567  26968  hbimpg  27373  gen11nv  27439  bnj1093  28059  ax12o10lem3X  28201  ax12o10lem3K  28202  ax12o10lem6K  28207  ax12o10lem6X  28208  ax12o10lem7K  28209  ax12o10lem7X  28210  ax12o10lem8K  28211  ax12o10lem8X  28212  ax12o10lem11K  28217  ax12o10lem11X  28218  ax12o10lem14K  28223  ax12o10lem14X  28224  ax12olem16K  28228  ax12olem16X  28229  ax12olem17K  28230  ax12olem17X  28231  ax12olem20K  28236  ax12olem20X  28237  ax10lem19X  28255  ax10lem24X  28260  a16gALTX  28265  ax9X  28269  hbae-x12  28276  ax10lem17ALT  28290  ax9lem3  28309  ax9lem6  28312  ax9lem8  28314  ax9lem9  28315  ax9lem10  28316  ax9lem12  28318  ax9lem13  28319  ax9lem17  28323  ax9vax9  28325
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