Theorem alrimivv 1928

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  2ax5  1937  2mo  2641  euind  3684  sbnfc2  4390  uniintsn  4935  eusvnf  5331  copsex2dv  5437  ssopab2dv  5494  ssrel  5726  relssdv  5731  eqrelrdv  5735  eqbrrdv  5736  eqrelrdv2  5738  ssrelrel  5739  iss  5986  iresn0n0  6005  ordelord  6329  suctr  6395  funssres  6526  funun  6528  fununi  6557  fsn  7069  ovg  7514  wemoiso  7908  wemoiso2  7909  oprabexd  7910  frrlem9  8227  omeu  8503  qliftfund  8730  eroveu  8739  fpwwe2lem10  10534  addsrmo  10967  mulsrmo  10968  seqf1o  13950  fi1uzind  14414  brfi1indALT  14417  summo  15624  prodmo  15843  pceu  16758  invfun  17671  initoeu2lem2  17922  psss  18486  psgneu  19385  gsumval3eu  19783  hausflimi  23865  vitalilem3  25509  plyexmo  26219  nosupprefixmo  27610  noinfprefixmo  27611  nosupno  27613  noinfno  27628  bdayon  28180  tglineintmo  28591  frgr3vlem1  30221  3vfriswmgrlem  30225  frgr2wwlk1  30277  pjhthmo  31250  chscl  31589  bnj1379  34813  bnj580  34896  bnj1321  35010  acycgr1v  35142  cvmlift2lem12  35307  satffunlem1lem1  35395  satffunlem2lem1  35397  mclsssvlem  35555  mclsax  35562  mclsind  35563  lineintmo  36151  trer  36310  mbfresfi  37666  unirep  37714  iss2  38332  prter1  38878  islpoldN  41483  ismrcd2  42692  ismrc  42694  tfsconcatb0  43337  mnutrd  44273  truniALT  44535  gen12  44612  sspwtrALT  44815  sspwtrALT2  44816  suctrALT  44819  suctrALT2  44830  trintALT  44874  suctrALTcf  44915  suctrALT3  44917  rlimdmafv  47181  rlimdmafv2  47262  opabresex0d  47289  spr0nelg  47480  sprsymrelfvlem  47494  mofsn  48848  thincmo  49433  functhincfun  49454