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

Theorem alrimdv 1697
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-5 1680 . 2  |-  ( ph  ->  A. x ph )
2 ax-5 1680 . 2  |-  ( ps 
->  A. x ps )
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimdh 1649 1  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem is referenced by:  axc9lem2  2013  zfpair  4684  fliftfun  6196  isofrlem  6222  funcnvuni  6734  f1oweALT  6765  findcard  7755  findcard2  7756  dfac5lem4  8503  dfac5  8505  zorn2lem4  8875  genpcl  9382  psslinpr  9405  ltaddpr  9408  ltexprlem3  9412  suplem1pr  9426  uzwo  11140  uzwoOLD  11141  seqf1o  12112  ramcl  14402  alexsubALTlem3  20284  truniALT  32392  ggen31  32397  onfrALTlem2  32398  gen21  32485  gen22  32488  ggen22  32489
  Copyright terms: Public domain W3C validator