Theorem alrimivv 1887

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

Syntax hints:   → wi 4  ∀wal 1505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem is referenced by:  2ax5  1896  2mo  2679  euind  3627  sbnfc2  4272  uniintsn  4786  eusvnf  5146  ssopab2dv  5290  ssrel  5507  relssdv  5511  eqrelrdv  5515  eqbrrdv  5516  eqrelrdv2  5518  ssrelrel  5519  iss  5748  ordelord  6051  suctr  6112  funssres  6231  funun  6233  fununi  6262  fsn  6720  opabresex2d  7027  fvmptopab  7028  ovg  7129  wemoiso  7486  wemoiso2  7487  oprabexd  7488  omeu  8012  qliftfund  8183  eroveu  8192  fpwwe2lem11  9860  addsrmo  10293  mulsrmo  10294  seqf1o  13226  fi1uzind  13666  brfi1indALT  13669  summo  14934  prodmo  15150  pceu  16039  invfun  16892  initoeu2lem2  17133  psss  17682  psgneu  18396  gsumval3eu  18778  hausflimi  22292  vitalilem3  23914  plyexmo  24605  tglineintmo  26130  frgr3vlem1  27807  3vfriswmgrlem  27811  frgr2wwlk1  27863  pjhthmo  28860  chscl  29199  bnj1379  31756  bnj580  31838  bnj1321  31950  cvmlift2lem12  32152  mclsssvlem  32335  mclsax  32342  mclsind  32343  frrlem9  32658  noprefixmo  32729  nosupno  32730  lineintmo  33145  trer  33191  mbfresfi  34385  unirep  34436  iss2  35053  prter1  35466  islpoldN  38071  ismrcd2  38697  ismrc  38699  mnutrd  39997  truniALT  40300  gen12  40377  sspwtrALT  40581  sspwtrALT2  40582  suctrALT  40585  suctrALT2  40596  trintALT  40640  suctrALTcf  40681  suctrALT3  40683  rlimdmafv  42788  rlimdmafv2  42869  opabresex0d  42896  spr0nelg  43012  sprsymrelfvlem  43026