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

Theorem alrimdv 2014
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  4106  funcnvuni  5174  fliftfun  5663  isofrlem  5689  f1oweALT  5703  findcard  6982  findcard2  6983  dfac5lem4  7637  dfac5  7639  zorn2lem4  8010  genpcl  8512  psslinpr  8535  ltaddpr  8538  ltexprlem3  8542  suplem1pr  8556  uzwo  10160  uzwoOLD  10161  seqf1o  10965  ramcl  12950  alexsubALTlem3  17575  truniALT  26998  ggen31  27003  onfrALTlem2  27004  gen21  27081  gen22  27084  ggen22  27085
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