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  13879  fi1uzind  14325  brfi1indALT  14328  summo  15538  prodmo  15755  pceu  16654  invfun  17583  initoeu2lem2  17837  psss  18405  psgneu  19223  gsumval3eu  19616  hausflimi  23259  vitalilem3  24902  plyexmo  25601  nosupprefixmo  26976  noinfprefixmo  26977  nosupno  26979  noinfno  26994  tglineintmo  27389  frgr3vlem1  29022  3vfriswmgrlem  29026  frgr2wwlk1  29078  pjhthmo  30049  chscl  30388  bnj1379  33222  bnj580  33305  bnj1321  33419  acycgr1v  33523  cvmlift2lem12  33688  satffunlem1lem1  33776  satffunlem2lem1  33778  mclsssvlem  33936  mclsax  33943  mclsind  33944  lineintmo  34673  trer  34719  mbfresfi  36055  unirep  36103  iss2  36736  prter1  37272  islpoldN  39878  ismrcd2  40924  ismrc  40926  mnutrd  42361  truniALT  42624  gen12  42701  sspwtrALT  42905  sspwtrALT2  42906  suctrALT  42909  suctrALT2  42920  trintALT  42964  suctrALTcf  43005  suctrALT3  43007  rlimdmafv  45200  rlimdmafv2  45281  opabresex0d  45308  spr0nelg  45459  sprsymrelfvlem  45473  mofsn  46701  thincmo  46840
  Copyright terms: Public domain W3C validator