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

Theorem alrimdv 1678
Description: Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.)
Hypothesis
Ref Expression
alrimdv.1
Assertion
Ref Expression
alrimdv
Distinct variable groups:   ,   ,

Proof of Theorem alrimdv
StepHypRef Expression
1 ax-5 1661 . 2
2 ax-5 1661 . 2
3 alrimdv.1 . 2
41, 2, 3alrimdh 1631 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1580
This theorem is referenced by:  axc9lem2  1979  zfpair  4501  fliftfun  5973  isofrlem  5999  funcnvuni  6499  f1oweALT  6530  findcard  7510  findcard2  7511  dfac5lem4  8243  dfac5  8245  zorn2lem4  8615  genpcl  9123  psslinpr  9146  ltaddpr  9149  ltexprlem3  9153  suplem1pr  9167  uzwo  10862  uzwoOLD  10863  seqf1o  11788  ramcl  14030  alexsubALTlem3  19325  truniALT  30825  ggen31  30830  onfrALTlem2  30831  gen21  30919  gen22  30922  ggen22  30923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1586  ax-4 1597  ax-5 1661
  Copyright terms: Public domain W3C validator