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

Theorem alrimivv 1720
 Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1905 and 19.21v 1729. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
alrimivv.1
Assertion
Ref Expression
alrimivv
Distinct variable groups:   ,   ,

Proof of Theorem alrimivv
StepHypRef Expression
1 alrimivv.1 . . 3
21alrimiv 1719 . 2
32alrimiv 1719 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  A.wal 1393 This theorem is referenced by:  2ax5  1728  2mo  2373  2moOLD  2374  euind  3286  sbnfc2  3854  uniintsn  4324  eusvnf  4647  ssopab2dv  4781  ordelord  4905  suctr  4966  ssrel  5096  relssdv  5100  eqrelrdv  5104  eqbrrdv  5105  eqrelrdv2  5107  ssrelrel  5108  iss  5326  funssres  5633  funun  5635  fununi  5659  fsn  6069  ovg  6441  wemoiso  6785  wemoiso2  6786  oprabexd  6787  omeu  7253  qliftfund  7416  eroveu  7425  fpwwe2lem11  9039  addsrmo  9471  mulsrmo  9472  seqf1o  12148  brfi1uzind  12532  swrd0  12658  summo  13539  prodmo  13743  pceu  14370  invfun  15158  psss  15844  psgneu  16531  gsumval3eu  16907  hausflimi  20481  vitalilem3  22019  plyexmo  22709  tglineintmo  24022  frgra3vlem1  25000  3vfriswmgralem  25004  frg2wot1  25057  2spotdisj  25061  pjhthmo  26220  chscl  26559  cvmlift2lem12  28759  mclsssvlem  28922  mclsax  28929  mclsind  28930  lineintmo  29807  mbfresfi  30061  trer  30134  unirep  30203  prter1  30620  ismrcd2  30631  ismrc  30633  rlimdmafv  32262  initoeu2lem2  32621  truniALT  33312  gen12  33404  sspwtrALT  33620  sspwtrALT2  33623  suctrALT  33626  suctrALT2  33637  trintALT  33681  suctrALTcf  33722  suctrALT3  33724  bnj1379  33889  bnj580  33971  bnj1321  34083  islpoldN  37211 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