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

Theorem alrimivv 1929
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2205 and 19.21v 1940. (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 1928 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1928 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem is referenced by:  2ax5  1938  2mo  2710  euind  3663  sbnfc2  4344  uniintsn  4875  eusvnf  5258  ssopab2dv  5403  ssrel  5621  relssdv  5625  eqrelrdv  5629  eqbrrdv  5630  eqrelrdv2  5632  ssrelrel  5633  iss  5870  iresn0n0  5890  ordelord  6181  suctr  6242  funssres  6368  funun  6370  fununi  6399  fsn  6874  opabresex2d  7187  fvmptopab  7188  ovg  7293  wemoiso  7656  wemoiso2  7657  oprabexd  7658  omeu  8194  qliftfund  8366  eroveu  8375  fpwwe2lem11  10051  addsrmo  10484  mulsrmo  10485  seqf1o  13407  fi1uzind  13851  brfi1indALT  13854  summo  15066  prodmo  15282  pceu  16173  invfun  17026  initoeu2lem2  17267  psss  17816  psgneu  18626  gsumval3eu  19017  hausflimi  22585  vitalilem3  24214  plyexmo  24909  tglineintmo  26436  frgr3vlem1  28058  3vfriswmgrlem  28062  frgr2wwlk1  28114  pjhthmo  29085  chscl  29424  bnj1379  32212  bnj580  32295  bnj1321  32409  acycgr1v  32509  cvmlift2lem12  32674  satffunlem1lem1  32762  satffunlem2lem1  32764  mclsssvlem  32922  mclsax  32929  mclsind  32930  frrlem9  33244  noprefixmo  33315  nosupno  33316  lineintmo  33731  trer  33777  mbfresfi  35103  unirep  35151  iss2  35761  prter1  36175  islpoldN  38780  ismrcd2  39638  ismrc  39640  mnutrd  40986  truniALT  41245  gen12  41322  sspwtrALT  41526  sspwtrALT2  41527  suctrALT  41530  suctrALT2  41541  trintALT  41585  suctrALTcf  41626  suctrALT3  41628  rlimdmafv  43731  rlimdmafv2  43812  opabresex0d  43839  spr0nelg  43991  sprsymrelfvlem  44005
  Copyright terms: Public domain W3C validator