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

Theorem alrimivv 1932
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2201 and 19.21v 1943. (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 1931 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1931 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem is referenced by:  2ax5  1941  2mo  2650  euind  3681  sbnfc2  4395  uniintsn  4947  eusvnf  5346  ssopab2dv  5506  ssrel  5735  ssrelOLD  5736  relssdv  5741  eqrelrdv  5745  eqbrrdv  5746  eqrelrdv2  5748  ssrelrel  5749  iss  5986  iresn0n0  6004  ordelord  6336  suctr  6400  funssres  6541  funun  6543  fununi  6572  fsn  7076  opabresex2d  7403  fvmptopabOLD  7405  ovg  7512  wemoiso  7897  wemoiso2  7898  oprabexd  7899  frrlem9  8193  omeu  8500  qliftfund  8676  eroveu  8685  fpwwe2lem10  10510  addsrmo  10943  mulsrmo  10944  seqf1o  13878  fi1uzind  14324  brfi1indALT  14327  summo  15537  prodmo  15754  pceu  16653  invfun  17582  initoeu2lem2  17836  psss  18404  psgneu  19221  gsumval3eu  19611  hausflimi  23254  vitalilem3  24897  plyexmo  25596  nosupprefixmo  26971  noinfprefixmo  26972  nosupno  26974  noinfno  26989  tglineintmo  27383  frgr3vlem1  29016  3vfriswmgrlem  29020  frgr2wwlk1  29072  pjhthmo  30043  chscl  30382  bnj1379  33216  bnj580  33299  bnj1321  33413  acycgr1v  33517  cvmlift2lem12  33682  satffunlem1lem1  33770  satffunlem2lem1  33772  mclsssvlem  33930  mclsax  33937  mclsind  33938  lineintmo  34638  trer  34684  mbfresfi  36020  unirep  36068  iss2  36701  prter1  37237  islpoldN  39843  ismrcd2  40888  ismrc  40890  mnutrd  42325  truniALT  42588  gen12  42665  sspwtrALT  42869  sspwtrALT2  42870  suctrALT  42873  suctrALT2  42884  trintALT  42928  suctrALTcf  42969  suctrALT3  42971  rlimdmafv  45164  rlimdmafv2  45245  opabresex0d  45272  spr0nelg  45423  sprsymrelfvlem  45437  mofsn  46665  thincmo  46804
  Copyright terms: Public domain W3C validator