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

Theorem alrimivv 1887
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2136 and 19.21v 1898. (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 1886 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1886 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem is referenced by:  2ax5  1896  2mo  2679  euind  3627  sbnfc2  4272  uniintsn  4786  eusvnf  5146  ssopab2dv  5290  ssrel  5507  relssdv  5511  eqrelrdv  5515  eqbrrdv  5516  eqrelrdv2  5518  ssrelrel  5519  iss  5748  ordelord  6051  suctr  6112  funssres  6231  funun  6233  fununi  6262  fsn  6720  opabresex2d  7027  fvmptopab  7028  ovg  7129  wemoiso  7486  wemoiso2  7487  oprabexd  7488  omeu  8012  qliftfund  8183  eroveu  8192  fpwwe2lem11  9860  addsrmo  10293  mulsrmo  10294  seqf1o  13226  fi1uzind  13666  brfi1indALT  13669  summo  14934  prodmo  15150  pceu  16039  invfun  16892  initoeu2lem2  17133  psss  17682  psgneu  18396  gsumval3eu  18778  hausflimi  22292  vitalilem3  23914  plyexmo  24605  tglineintmo  26130  frgr3vlem1  27807  3vfriswmgrlem  27811  frgr2wwlk1  27863  pjhthmo  28860  chscl  29199  bnj1379  31756  bnj580  31838  bnj1321  31950  cvmlift2lem12  32152  mclsssvlem  32335  mclsax  32342  mclsind  32343  frrlem9  32658  noprefixmo  32729  nosupno  32730  lineintmo  33145  trer  33191  mbfresfi  34385  unirep  34436  iss2  35053  prter1  35466  islpoldN  38071  ismrcd2  38697  ismrc  38699  mnutrd  39997  truniALT  40300  gen12  40377  sspwtrALT  40581  sspwtrALT2  40582  suctrALT  40585  suctrALT2  40596  trintALT  40640  suctrALTcf  40681  suctrALT3  40683  rlimdmafv  42788  rlimdmafv2  42869  opabresex0d  42896  spr0nelg  43012  sprsymrelfvlem  43026
  Copyright terms: Public domain W3C validator