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  3695  sbnfc2  4402  uniintsn  4949  eusvnf  5347  copsex2dv  5454  ssopab2dv  5511  ssrel  5745  ssrelOLD  5746  relssdv  5751  eqrelrdv  5755  eqbrrdv  5756  eqrelrdv2  5758  ssrelrel  5759  iss  6006  iresn0n0  6025  ordelord  6354  suctr  6420  funssres  6560  funun  6562  fununi  6591  fsn  7107  opabresex2d  7442  fvmptopabOLD  7444  ovg  7554  wemoiso  7952  wemoiso2  7953  oprabexd  7954  frrlem9  8273  omeu  8549  qliftfund  8776  eroveu  8785  fpwwe2lem10  10593  addsrmo  11026  mulsrmo  11027  seqf1o  14008  fi1uzind  14472  brfi1indALT  14475  summo  15683  prodmo  15902  pceu  16817  invfun  17726  initoeu2lem2  17977  psss  18539  psgneu  19436  gsumval3eu  19834  hausflimi  23867  vitalilem3  25511  plyexmo  26221  nosupprefixmo  27612  noinfprefixmo  27613  nosupno  27615  noinfno  27630  bdayon  28173  tglineintmo  28569  frgr3vlem1  30202  3vfriswmgrlem  30206  frgr2wwlk1  30258  pjhthmo  31231  chscl  31570  bnj1379  34820  bnj580  34903  bnj1321  35017  acycgr1v  35136  cvmlift2lem12  35301  satffunlem1lem1  35389  satffunlem2lem1  35391  mclsssvlem  35549  mclsax  35556  mclsind  35557  lineintmo  36145  trer  36304  mbfresfi  37660  unirep  37708  iss2  38326  prter1  38872  islpoldN  41478  ismrcd2  42687  ismrc  42689  tfsconcatb0  43333  mnutrd  44269  truniALT  44531  gen12  44608  sspwtrALT  44811  sspwtrALT2  44812  suctrALT  44815  suctrALT2  44826  trintALT  44870  suctrALTcf  44911  suctrALT3  44913  rlimdmafv  47178  rlimdmafv2  47259  opabresex0d  47286  spr0nelg  47477  sprsymrelfvlem  47491  mofsn  48832  thincmo  49417  functhincfun  49438