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

Theorem alrimdv 1640
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 1623 . 2  |-  ( ph  ->  A. x ph )
2 ax-17 1623 . 2  |-  ( ps 
->  A. x ps )
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimdh 1594 1  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546
This theorem is referenced by:  ax12olem2  1973  zfpair  4361  funcnvuni  5477  fliftfun  5993  isofrlem  6019  f1oweALT  6033  findcard  7306  findcard2  7307  dfac5lem4  7963  dfac5  7965  zorn2lem4  8335  genpcl  8841  psslinpr  8864  ltaddpr  8867  ltexprlem3  8871  suplem1pr  8885  uzwo  10495  uzwoOLD  10496  seqf1o  11319  ramcl  13352  alexsubALTlem3  18033  truniALT  28337  ggen31  28342  onfrALTlem2  28343  gen21  28429  gen22  28432  ggen22  28433
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
  Copyright terms: Public domain W3C validator