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

Theorem alrimivv 1969
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2186 and 19.21v 1981. (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 1968 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1968 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1835  ax-4 1850  ax-5 1952
This theorem is referenced by:  2ax5  1979  2mo  2653  euind  3499  sbnfc2  4115  uniintsn  4622  eusvnf  4966  ssopab2dv  5108  ssrel  5316  ssrelOLD  5317  relssdv  5321  eqrelrdv  5325  eqbrrdv  5326  eqrelrdv2  5328  ssrelrel  5329  iss  5557  ordelord  5858  suctr  5921  suctrOLD  5922  funssres  6043  funun  6045  fununi  6077  fsn  6517  opabresex2d  6813  fvmptopab  6814  ovg  6916  wemoiso  7270  wemoiso2  7271  oprabexd  7272  omeu  7785  qliftfund  7951  eroveu  7960  fpwwe2lem11  9575  addsrmo  10007  mulsrmo  10008  seqf1o  12957  fi1uzind  13392  brfi1indALT  13395  summo  14568  prodmo  14786  pceu  15674  invfun  16546  initoeu2lem2  16787  psss  17336  psgneu  18047  gsumval3eu  18426  hausflimi  21906  vitalilem3  23499  plyexmo  24188  tglineintmo  25657  frgr3vlem1  27348  3vfriswmgrlem  27352  frgr2wwlk1  27404  pjhthmo  28391  chscl  28730  bnj1379  31129  bnj580  31211  bnj1321  31323  cvmlift2lem12  31524  mclsssvlem  31687  mclsax  31694  mclsind  31695  noprefixmo  32075  nosupno  32076  lineintmo  32491  trer  32537  mbfresfi  33688  unirep  33739  iss2  34354  prter1  34585  islpoldN  37192  ismrcd2  37681  ismrc  37683  truniALT  39170  gen12  39262  sspwtrALT  39468  sspwtrALT2  39474  suctrALT  39477  suctrALT2  39488  trintALT  39533  suctrALTcf  39574  suctrALT3  39576  rlimdmafv  41680  opabresex0d  41729  spr0nelg  42153  sprsymrelfvlem  42167
  Copyright terms: Public domain W3C validator