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

Theorem alrimdv 1721
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1905 and 19.21v 1729. (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 1704 . 2
2 ax-5 1704 . 2
3 alrimdv.1 . 2
41, 2, 3alrimdh 1672 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393
This theorem is referenced by:  axc9lem2  2040  zfpair  4689  fliftfun  6210  isofrlem  6236  funcnvuni  6753  f1oweALT  6784  findcard  7779  findcard2  7780  dfac5lem4  8528  dfac5  8530  zorn2lem4  8900  genpcl  9407  psslinpr  9430  ltaddpr  9433  ltexprlem3  9437  suplem1pr  9451  uzwo  11173  uzwoOLD  11174  seqf1o  12148  ramcl  14547  alexsubALTlem3  20549  truniALT  33312  ggen31  33317  onfrALTlem2  33318  gen21  33405  gen22  33408  ggen22  33409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1618  ax-4 1631  ax-5 1704
  Copyright terms: Public domain W3C validator