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

Theorem alrimivv 1842
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2060 and 19.21v 1854. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
alrimivv.1 (𝜑𝜓)
Assertion
Ref Expression
alrimivv (𝜑 → ∀𝑥𝑦𝜓)
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem alrimivv
StepHypRef Expression
1 alrimivv.1 . . 3 (𝜑𝜓)
21alrimiv 1841 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1841 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem is referenced by:  2ax5  1852  2mo  2538  euind  3359  sbnfc2  3958  uniintsn  4443  eusvnf  4782  ssopab2dv  4919  ssrel  5120  relssdv  5124  eqrelrdv  5128  eqbrrdv  5129  eqrelrdv2  5131  ssrelrel  5132  iss  5354  ordelord  5648  suctr  5711  suctrOLD  5712  funssres  5830  funun  5832  fununi  5864  fsn  6293  ovg  6675  wemoiso  7021  wemoiso2  7022  oprabexd  7023  omeu  7529  qliftfund  7697  eroveu  7706  fpwwe2lem11  9318  addsrmo  9750  mulsrmo  9751  seqf1o  12659  fi1uzind  13080  brfi1indALT  13083  fi1uzindOLD  13086  brfi1indALTOLD  13089  summo  14241  prodmo  14451  pceu  15335  invfun  16193  initoeu2lem2  16434  psss  16983  psgneu  17695  gsumval3eu  18074  hausflimi  21536  vitalilem3  23102  plyexmo  23789  tglineintmo  25255  frgra3vlem1  26293  3vfriswmgralem  26297  frg2wot1  26350  2spotdisj  26354  pjhthmo  27351  chscl  27690  bnj1379  29961  bnj580  30043  bnj1321  30155  cvmlift2lem12  30356  mclsssvlem  30519  mclsax  30526  mclsind  30527  lineintmo  31240  trer  31286  mbfresfi  32429  unirep  32480  prter1  32985  islpoldN  35594  ismrcd2  36083  ismrc  36085  truniALT  37575  gen12  37667  sspwtrALT  37874  sspwtrALT2  37883  suctrALT  37886  suctrALT2  37897  trintALT  37942  suctrALTcf  37983  suctrALT3  37985  rlimdmafv  39711  opabresex0d  40157  opabresex2d  40161  frgr3vlem1  41445  3vfriswmgrlem  41449  frgr2wwlk1  41496
  Copyright terms: Public domain W3C validator