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

Theorem alrimivv 1931
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2200 and 19.21v 1942. (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 1930 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1930 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1913
This theorem is referenced by:  2ax5  1940  2mo  2648  euind  3680  sbnfc2  4394  uniintsn  4946  eusvnf  5345  ssopab2dv  5506  ssrel  5736  ssrelOLD  5737  relssdv  5742  eqrelrdv  5746  eqbrrdv  5747  eqrelrdv2  5749  ssrelrel  5750  iss  5987  iresn0n0  6005  ordelord  6337  suctr  6401  funssres  6542  funun  6544  fununi  6573  fsn  7077  opabresex2d  7406  fvmptopabOLD  7408  ovg  7515  wemoiso  7902  wemoiso2  7903  oprabexd  7904  frrlem9  8221  omeu  8528  qliftfund  8738  eroveu  8747  fpwwe2lem10  10572  addsrmo  11005  mulsrmo  11006  seqf1o  13941  fi1uzind  14388  brfi1indALT  14391  summo  15594  prodmo  15811  pceu  16710  invfun  17639  initoeu2lem2  17893  psss  18461  psgneu  19279  gsumval3eu  19672  hausflimi  23315  vitalilem3  24958  plyexmo  25657  nosupprefixmo  27032  noinfprefixmo  27033  nosupno  27035  noinfno  27050  tglineintmo  27470  frgr3vlem1  29103  3vfriswmgrlem  29107  frgr2wwlk1  29159  pjhthmo  30130  chscl  30469  bnj1379  33311  bnj580  33394  bnj1321  33508  acycgr1v  33612  cvmlift2lem12  33777  satffunlem1lem1  33865  satffunlem2lem1  33867  mclsssvlem  34025  mclsax  34032  mclsind  34033  lineintmo  34709  trer  34755  mbfresfi  36091  unirep  36139  iss2  36772  prter1  37308  islpoldN  39914  ismrcd2  40960  ismrc  40962  mnutrd  42502  truniALT  42765  gen12  42842  sspwtrALT  43046  sspwtrALT2  43047  suctrALT  43050  suctrALT2  43061  trintALT  43105  suctrALTcf  43146  suctrALT3  43148  rlimdmafv  45341  rlimdmafv2  45422  opabresex0d  45449  spr0nelg  45600  sprsymrelfvlem  45614  mofsn  46842  thincmo  46981
  Copyright terms: Public domain W3C validator