Theorem alrimivv 1929

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2210 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

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem is referenced by:  2ax5  1938  2mo  2643  euind  3678  sbnfc2  4386  uniintsn  4933  eusvnf  5328  copsex2dv  5432  ssopab2dv  5489  ssrel  5722  relssdv  5727  eqrelrdv  5731  eqbrrdv  5732  eqrelrdv2  5734  ssrelrel  5735  iss  5983  iresn0n0  6002  ordelord  6328  suctr  6394  funssres  6525  funun  6527  fununi  6556  fsn  7068  ovg  7511  wemoiso  7905  wemoiso2  7906  oprabexd  7907  frrlem9  8224  omeu  8500  qliftfund  8727  eroveu  8736  fpwwe2lem10  10531  addsrmo  10964  mulsrmo  10965  seqf1o  13950  fi1uzind  14414  brfi1indALT  14417  summo  15624  prodmo  15843  pceu  16758  invfun  17671  initoeu2lem2  17922  psss  18486  psgneu  19418  gsumval3eu  19816  hausflimi  23895  vitalilem3  25538  plyexmo  26248  nosupprefixmo  27639  noinfprefixmo  27640  nosupno  27642  noinfno  27657  bdayon  28209  tglineintmo  28620  frgr3vlem1  30253  3vfriswmgrlem  30257  frgr2wwlk1  30309  pjhthmo  31282  chscl  31621  bnj1379  34842  bnj580  34925  bnj1321  35039  acycgr1v  35193  cvmlift2lem12  35358  satffunlem1lem1  35446  satffunlem2lem1  35448  mclsssvlem  35606  mclsax  35613  mclsind  35614  lineintmo  36201  trer  36360  mbfresfi  37705  unirep  37753  iss2  38375  prter1  38977  islpoldN  41582  ismrcd2  42791  ismrc  42793  tfsconcatb0  43436  mnutrd  44372  truniALT  44633  gen12  44710  sspwtrALT  44913  sspwtrALT2  44914  suctrALT  44917  suctrALT2  44928  trintALT  44972  suctrALTcf  45013  suctrALT3  45015  rlimdmafv  47276  rlimdmafv2  47357  opabresex0d  47384  spr0nelg  47575  sprsymrelfvlem  47589  mofsn  48943  thincmo  49528  functhincfun  49549