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

Theorem alrimdv 1623
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 1606 . 2  |-  ( ph  ->  A. x ph )
2 ax-17 1606 . 2  |-  ( ps 
->  A. x ps )
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimdh 1577 1  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  zfpair  4228  funcnvuni  5333  fliftfun  5827  isofrlem  5853  f1oweALT  5867  findcard  7113  findcard2  7114  dfac5lem4  7769  dfac5  7771  zorn2lem4  8142  genpcl  8648  psslinpr  8671  ltaddpr  8674  ltexprlem3  8678  suplem1pr  8692  uzwo  10297  uzwoOLD  10298  seqf1o  11103  ramcl  13092  alexsubALTlem3  17759  truniALT  28604  ggen31  28609  onfrALTlem2  28610  gen21  28696  gen22  28699  ggen22  28700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
  Copyright terms: Public domain W3C validator