Theorem alrimivv 2023

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

Syntax hints:   → wi 4  ∀wal 1650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1890  ax-4 1904  ax-5 2005

This theorem is referenced by:  2ax5  2032  2mo  2673  euind  3552  sbnfc2  4169  uniintsn  4670  eusvnf  5027  ssopab2dv  5165  ssrel  5377  relssdv  5381  eqrelrdv  5385  eqbrrdv  5386  eqrelrdv2  5388  ssrelrel  5389  iss  5624  ordelord  5930  suctr  5991  funssres  6111  funun  6113  fununi  6142  fsn  6593  opabresex2d  6894  fvmptopab  6895  ovg  6997  wemoiso  7351  wemoiso2  7352  oprabexd  7353  omeu  7870  qliftfund  8036  eroveu  8046  fpwwe2lem11  9715  addsrmo  10147  mulsrmo  10148  seqf1o  13049  fi1uzind  13480  brfi1indALT  13483  summo  14735  prodmo  14951  pceu  15832  invfun  16691  initoeu2lem2  16932  psss  17482  psgneu  18192  gsumval3eu  18571  hausflimi  22063  vitalilem3  23668  plyexmo  24359  tglineintmo  25828  frgr3vlem1  27511  3vfriswmgrlem  27515  frgr2wwlk1  27567  pjhthmo  28552  chscl  28891  bnj1379  31281  bnj580  31363  bnj1321  31475  cvmlift2lem12  31676  mclsssvlem  31839  mclsax  31846  mclsind  31847  noprefixmo  32224  nosupno  32225  lineintmo  32640  trer  32686  mbfresfi  33811  unirep  33862  iss2  34473  prter1  34767  islpoldN  37372  ismrcd2  37872  ismrc  37874  truniALT  39351  gen12  39437  sspwtrALT  39642  sspwtrALT2  39643  suctrALT  39646  suctrALT2  39657  trintALT  39701  suctrALTcf  39742  suctrALT3  39744  rlimdmafv  41857  rlimdmafv2  41938  opabresex0d  41966  spr0nelg  42327  sprsymrelfvlem  42341