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

Theorem alrimdv 1686
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-5 1669 . 2  |-  ( ph  ->  A. x ph )
2 ax-5 1669 . 2  |-  ( ps 
->  A. x ps )
3 alrimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3alrimdh 1639 1  |-  ( ph  ->  ( ps  ->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1594  ax-4 1605  ax-5 1669
This theorem is referenced by:  axc9lem2  1987  zfpair  4517  fliftfun  5992  isofrlem  6018  funcnvuni  6519  f1oweALT  6550  findcard  7539  findcard2  7540  dfac5lem4  8284  dfac5  8286  zorn2lem4  8656  genpcl  9165  psslinpr  9188  ltaddpr  9191  ltexprlem3  9195  suplem1pr  9209  uzwo  10905  uzwoOLD  10906  seqf1o  11831  ramcl  14073  alexsubALTlem3  19463  truniALT  30970  ggen31  30975  onfrALTlem2  30976  gen21  31064  gen22  31067  ggen22  31068
  Copyright terms: Public domain W3C validator