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

Theorem alrimdv 1688
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 1671 . 2
2 ax-5 1671 . 2
3 alrimdv.1 . 2
41, 2, 3alrimdh 1640 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1368
This theorem is referenced by:  axc9lem2  2000  zfpair  4646  fliftfun  6136  isofrlem  6162  funcnvuni  6663  f1oweALT  6694  findcard  7686  findcard2  7687  dfac5lem4  8433  dfac5  8435  zorn2lem4  8805  genpcl  9314  psslinpr  9337  ltaddpr  9340  ltexprlem3  9344  suplem1pr  9358  uzwo  11056  uzwoOLD  11057  seqf1o  12004  ramcl  14248  alexsubALTlem3  20020  truniALT  32091  ggen31  32096  onfrALTlem2  32097  gen21  32184  gen22  32187  ggen22  32188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1592  ax-4 1603  ax-5 1671
  Copyright terms: Public domain W3C validator