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 1547 . 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 1528
This theorem is referenced by:  eximdh  1576  nexdh  1577  albidh  1578  exbidh  1579  alrimiv  1618  ax11i  1629  ax11f  1630  cbvaliw  1643  hbn  1721  hbimd  1722  spimeh  1723  hbim  1726  19.23h  1729  equsalhw  1731  19.21h  1732  19.12  1735  cbv3hv  1738  alrimi  1746  hbnd  1825  dvelimv  1880  a16gALT  1886  a5i-o  2091  equidq  2116  aev-o  2123  eujustALT  2147  ceqsex3OLD  26125  ax4567  27000  hbimpg  27591  gen11nv  27657  bnj1093  28277  hbae-x12  28376  ax10lem17ALT  28390  ax9lem3  28409  ax9lem6  28412  ax9lem8  28414  ax9lem9  28415  ax9lem10  28416  ax9lem12  28418  ax9lem13  28419  ax9lem17  28423  ax9vax9  28425
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10  ax-gen 1534  ax-5 1545
  Copyright terms: Public domain W3C validator