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  1851  aev-o  1924  ax11f  2107  eujustALT  2117  ceqsex3OLD  25892  ax4567  26767  hbimpg  27013  gen11nv  27079  bnj1093  27699  hbae-x12  27798  ax10lem17ALT  27812  ax9lem3  27831  ax9lem6  27834  ax9lem8  27836  ax9lem9  27837  ax9lem10  27838  ax9lem12  27840  ax9lem13  27841  ax9lem17  27845  ax9vax9  27847
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