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

Theorem alrimdv 1624
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 1608 . 2  |-  ( ph  ->  A. x ph )
2 ax-17 1608 . 2  |-  ( ps 
->  A. x ps )
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimdh 1579 1  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532
This theorem is referenced by:  zfpair  4211  funcnvuni  5282  fliftfun  5772  isofrlem  5798  f1oweALT  5812  findcard  7092  findcard2  7093  dfac5lem4  7748  dfac5  7750  zorn2lem4  8121  genpcl  8627  psslinpr  8650  ltaddpr  8653  ltexprlem3  8657  suplem1pr  8671  uzwo  10276  uzwoOLD  10277  seqf1o  11081  ramcl  13070  alexsubALTlem3  17737  truniALT  27576  ggen31  27581  onfrALTlem2  27582  gen21  27659  gen22  27662  ggen22  27663
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608
  Copyright terms: Public domain W3C validator