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

Theorem alrimdv 1643
Description: Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.)
Hypothesis
Ref Expression
alrimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
alrimdv  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Distinct variable groups:    ph, x    ps, x
Allowed substitution hint:    ch( x)

Proof of Theorem alrimdv
StepHypRef Expression
1 ax-17 1626 . 2  |-  ( ph  ->  A. x ph )
2 ax-17 1626 . 2  |-  ( ps 
->  A. x ps )
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimdh 1597 1  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549
This theorem is referenced by:  ax12olem2  2006  zfpair  4393  funcnvuni  5509  fliftfun  6025  isofrlem  6051  f1oweALT  6065  findcard  7338  findcard2  7339  dfac5lem4  7996  dfac5  7998  zorn2lem4  8368  genpcl  8874  psslinpr  8897  ltaddpr  8900  ltexprlem3  8904  suplem1pr  8918  uzwo  10528  uzwoOLD  10529  seqf1o  11352  ramcl  13385  alexsubALTlem3  18068  truniALT  28481  ggen31  28486  onfrALTlem2  28487  gen21  28574  gen22  28577  ggen22  28578
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
  Copyright terms: Public domain W3C validator