Theorem alrimivv 1932

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2203 and 19.21v 1943. (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 1931	. 2 ⊢ (𝜑 → ∀𝑦𝜓)
3	2	alrimiv 1931	1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem is referenced by:  2ax5  1941  2mo  2650  euind  3654  sbnfc2  4367  uniintsn  4915  eusvnf  5310  ssopab2dv  5457  ssrel  5683  relssdv  5687  eqrelrdv  5691  eqbrrdv  5692  eqrelrdv2  5694  ssrelrel  5695  iss  5932  iresn0n0  5952  ordelord  6273  suctr  6334  funssres  6462  funun  6464  fununi  6493  fsn  6989  opabresex2d  7307  fvmptopab  7308  ovg  7415  wemoiso  7789  wemoiso2  7790  oprabexd  7791  frrlem9  8081  omeu  8378  qliftfund  8550  eroveu  8559  fpwwe2lem10  10327  addsrmo  10760  mulsrmo  10761  seqf1o  13692  fi1uzind  14139  brfi1indALT  14142  summo  15357  prodmo  15574  pceu  16475  invfun  17393  initoeu2lem2  17646  psss  18213  psgneu  19029  gsumval3eu  19420  hausflimi  23039  vitalilem3  24679  plyexmo  25378  tglineintmo  26907  frgr3vlem1  28538  3vfriswmgrlem  28542  frgr2wwlk1  28594  pjhthmo  29565  chscl  29904  bnj1379  32710  bnj580  32793  bnj1321  32907  acycgr1v  33011  cvmlift2lem12  33176  satffunlem1lem1  33264  satffunlem2lem1  33266  mclsssvlem  33424  mclsax  33431  mclsind  33432  nosupprefixmo  33830  noinfprefixmo  33831  nosupno  33833  noinfno  33848  lineintmo  34386  trer  34432  mbfresfi  35750  unirep  35798  iss2  36406  prter1  36820  islpoldN  39425  ismrcd2  40437  ismrc  40439  mnutrd  41787  truniALT  42050  gen12  42127  sspwtrALT  42331  sspwtrALT2  42332  suctrALT  42335  suctrALT2  42346  trintALT  42390  suctrALTcf  42431  suctrALT3  42433  rlimdmafv  44556  rlimdmafv2  44637  opabresex0d  44664  spr0nelg  44816  sprsymrelfvlem  44830  mofsn  46059  thincmo  46198