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  4150  funcnvuni  5220  fliftfun  5710  isofrlem  5736  f1oweALT  5750  findcard  7030  findcard2  7031  dfac5lem4  7686  dfac5  7688  zorn2lem4  8059  genpcl  8565  psslinpr  8588  ltaddpr  8591  ltexprlem3  8595  suplem1pr  8609  uzwo  10213  uzwoOLD  10214  seqf1o  11018  ramcl  13003  alexsubALTlem3  17670  truniALT  27321  ggen31  27326  onfrALTlem2  27327  gen21  27404  gen22  27407  ggen22  27408
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