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

Theorem alrimih 1552
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 15 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527
This theorem is referenced by:  eximdh  1575  nexdh  1576  albidh  1577  exbidh  1578  alrimiv  1617  ax11i  1628  cbvaliw  1641  hbn  1720  hbimd  1721  spimeh  1722  hbim  1725  19.23h  1728  equsalhw  1730  19.21h  1731  19.12  1734  cbv3hv  1737  alrimi  1745  hbnd  1824  dvelimv  1879  a16g  1885  aev  1931  a5i-o  2089  equidq  2114  aev-o  2121  ax11f  2131  eujustALT  2146  ceqsex3OLD  26726  ax4567  27601  hbimpg  28320  gen11nv  28389  bnj1093  29010  hbae-x12  29109  ax10lem17ALT  29123  ax9lem3  29142  ax9lem6  29145  ax9lem8  29147  ax9lem9  29148  ax9lem10  29149  ax9lem12  29151  ax9lem13  29152  ax9lem17  29156  ax9vax9  29158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1533  ax-5 1544
  Copyright terms: Public domain W3C validator