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

Theorem alrimdv 2015
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 nfv 1629 . 2  |-  F/ x ph
2 nfv 1629 . 2  |-  F/ x ps
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimd 1710 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  4184  funcnvuni  5255  fliftfun  5745  isofrlem  5771  f1oweALT  5785  findcard  7065  findcard2  7066  dfac5lem4  7721  dfac5  7723  zorn2lem4  8094  genpcl  8600  psslinpr  8623  ltaddpr  8626  ltexprlem3  8630  suplem1pr  8644  uzwo  10248  uzwoOLD  10249  seqf1o  11053  ramcl  13038  alexsubALTlem3  17705  truniALT  27358  ggen31  27363  onfrALTlem2  27364  gen21  27441  gen22  27444  ggen22  27445
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540
  Copyright terms: Public domain W3C validator