Theorem alrimivv 1929

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

Syntax hints:   → wi 4  ∀wal 1537

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

This theorem is referenced by:  2ax5  1938  2mo  2642  euind  3719  sbnfc2  4435  uniintsn  4990  eusvnf  5389  ssopab2dv  5550  ssrel  5781  ssrelOLD  5782  relssdv  5787  eqrelrdv  5791  eqbrrdv  5792  eqrelrdv2  5794  ssrelrel  5795  iss  6034  iresn0n0  6052  ordelord  6385  suctr  6449  funssres  6591  funun  6593  fununi  6622  fsn  7134  opabresex2d  7464  fvmptopabOLD  7466  ovg  7574  wemoiso  7962  wemoiso2  7963  oprabexd  7964  frrlem9  8281  omeu  8587  qliftfund  8799  eroveu  8808  fpwwe2lem10  10637  addsrmo  11070  mulsrmo  11071  seqf1o  14013  fi1uzind  14462  brfi1indALT  14465  summo  15667  prodmo  15884  pceu  16783  invfun  17715  initoeu2lem2  17969  psss  18537  psgneu  19415  gsumval3eu  19813  hausflimi  23704  vitalilem3  25359  plyexmo  26062  nosupprefixmo  27439  noinfprefixmo  27440  nosupno  27442  noinfno  27457  tglineintmo  28160  frgr3vlem1  29793  3vfriswmgrlem  29797  frgr2wwlk1  29849  pjhthmo  30822  chscl  31161  bnj1379  34139  bnj580  34222  bnj1321  34336  acycgr1v  34438  cvmlift2lem12  34603  satffunlem1lem1  34691  satffunlem2lem1  34693  mclsssvlem  34851  mclsax  34858  mclsind  34859  lineintmo  35433  trer  35504  mbfresfi  36837  unirep  36885  iss2  37516  prter1  38052  islpoldN  40658  ismrcd2  41739  ismrc  41741  tfsconcatb0  42396  mnutrd  43341  truniALT  43604  gen12  43681  sspwtrALT  43885  sspwtrALT2  43886  suctrALT  43889  suctrALT2  43900  trintALT  43944  suctrALTcf  43985  suctrALT3  43987  rlimdmafv  46183  rlimdmafv2  46264  opabresex0d  46291  spr0nelg  46442  sprsymrelfvlem  46456  mofsn  47597  thincmo  47736