Theorem alrimivv 1924

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2196 and 19.21v 1935. (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

Step	Hyp	Ref	Expression
1		alrimivv.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	alrimiv 1923	. 2 ⊢ (𝜑 → ∀𝑦𝜓)
3	2	alrimiv 1923	1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem is referenced by:  2ax5  1933  2mo  2637  euind  3718  sbnfc2  4441  uniintsn  4997  eusvnf  5398  ssopab2dv  5559  ssrel  5790  ssrelOLD  5791  relssdv  5796  eqrelrdv  5800  eqbrrdv  5801  eqrelrdv2  5803  ssrelrel  5804  iss  6046  iresn0n0  6065  ordelord  6400  suctr  6464  funssres  6605  funun  6607  fununi  6636  fsn  7151  opabresex2d  7480  fvmptopabOLD  7482  ovg  7593  wemoiso  7989  wemoiso2  7990  oprabexd  7991  frrlem9  8311  omeu  8617  qliftfund  8834  eroveu  8843  fpwwe2lem10  10685  addsrmo  11118  mulsrmo  11119  seqf1o  14065  fi1uzind  14518  brfi1indALT  14521  summo  15723  prodmo  15940  pceu  16850  invfun  17782  initoeu2lem2  18039  psss  18607  psgneu  19506  gsumval3eu  19904  hausflimi  23978  vitalilem3  25633  plyexmo  26344  nosupprefixmo  27733  noinfprefixmo  27734  nosupno  27736  noinfno  27751  tglineintmo  28572  frgr3vlem1  30209  3vfriswmgrlem  30213  frgr2wwlk1  30265  pjhthmo  31238  chscl  31577  copsex2dv  32528  bnj1379  34677  bnj580  34760  bnj1321  34874  acycgr1v  34979  cvmlift2lem12  35144  satffunlem1lem1  35232  satffunlem2lem1  35234  mclsssvlem  35392  mclsax  35399  mclsind  35400  lineintmo  35983  trer  36030  mbfresfi  37369  unirep  37417  iss2  38044  prter1  38579  islpoldN  41185  ismrcd2  42374  ismrc  42376  tfsconcatb0  43028  mnutrd  43972  truniALT  44235  gen12  44312  sspwtrALT  44516  sspwtrALT2  44517  suctrALT  44520  suctrALT2  44531  trintALT  44575  suctrALTcf  44616  suctrALT3  44618  rlimdmafv  46808  rlimdmafv2  46889  opabresex0d  46916  spr0nelg  47066  sprsymrelfvlem  47080  mofsn  48229  thincmo  48368