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

Theorem alrimdv 1619
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 1603 . 2  |-  ( ph  ->  A. x ph )
2 ax-17 1603 . 2  |-  ( ps 
->  A. x ps )
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimdh 1574 1  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527
This theorem is referenced by:  zfpair  4212  funcnvuni  5317  fliftfun  5811  isofrlem  5837  f1oweALT  5851  findcard  7097  findcard2  7098  dfac5lem4  7753  dfac5  7755  zorn2lem4  8126  genpcl  8632  psslinpr  8655  ltaddpr  8658  ltexprlem3  8662  suplem1pr  8676  uzwo  10281  uzwoOLD  10282  seqf1o  11087  ramcl  13076  alexsubALTlem3  17743  truniALT  28305  ggen31  28310  onfrALTlem2  28311  gen21  28391  gen22  28394  ggen22  28395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
  Copyright terms: Public domain W3C validator