Theorem alrimivv 1896

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

Syntax hints:   → wi 4  ∀wal 1521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem is referenced by:  2ax5  1906  2mo  2580  euind  3426  sbnfc2  4040  uniintsn  4546  eusvnf  4891  ssopab2dv  5033  ssrel  5241  ssrelOLD  5242  relssdv  5246  eqrelrdv  5250  eqbrrdv  5251  eqrelrdv2  5253  ssrelrel  5254  iss  5482  ordelord  5783  suctr  5846  suctrOLD  5847  funssres  5968  funun  5970  fununi  6002  fsn  6442  opabresex2d  6738  fvmptopab  6739  ovg  6841  wemoiso  7195  wemoiso2  7196  oprabexd  7197  omeu  7710  qliftfund  7876  eroveu  7885  fpwwe2lem11  9500  addsrmo  9932  mulsrmo  9933  seqf1o  12882  fi1uzind  13317  brfi1indALT  13320  summo  14492  prodmo  14710  pceu  15598  invfun  16471  initoeu2lem2  16712  psss  17261  psgneu  17972  gsumval3eu  18351  hausflimi  21831  vitalilem3  23424  plyexmo  24113  tglineintmo  25582  frgr3vlem1  27253  3vfriswmgrlem  27257  frgr2wwlk1  27309  pjhthmo  28289  chscl  28628  bnj1379  31027  bnj580  31109  bnj1321  31221  cvmlift2lem12  31422  mclsssvlem  31585  mclsax  31592  mclsind  31593  noprefixmo  31973  nosupno  31974  lineintmo  32389  trer  32435  mbfresfi  33586  unirep  33637  iss2  34252  prter1  34483  islpoldN  37090  ismrcd2  37579  ismrc  37581  truniALT  39068  gen12  39160  sspwtrALT  39366  sspwtrALT2  39372  suctrALT  39375  suctrALT2  39386  trintALT  39431  suctrALTcf  39472  suctrALT3  39474  rlimdmafv  41578  opabresex0d  41627  spr0nelg  42051  sprsymrelfvlem  42065