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

Theorem alrimdv 1687
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 1670 . 2  |-  ( ph  ->  A. x ph )
2 ax-5 1670 . 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 1367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1591  ax-4 1602  ax-5 1670
This theorem is referenced by:  axc9lem2  1988  zfpair  4532  fliftfun  6008  isofrlem  6034  funcnvuni  6533  f1oweALT  6564  findcard  7554  findcard2  7555  dfac5lem4  8299  dfac5  8301  zorn2lem4  8671  genpcl  9180  psslinpr  9203  ltaddpr  9206  ltexprlem3  9210  suplem1pr  9224  uzwo  10920  uzwoOLD  10921  seqf1o  11850  ramcl  14093  alexsubALTlem3  19624  truniALT  31251  ggen31  31256  onfrALTlem2  31257  gen21  31344  gen22  31347  ggen22  31348
  Copyright terms: Public domain W3C validator