Theorem alrimivv 1961

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1828  ax-4 1842  ax-5 1943

This theorem is used by:  2ax5  1970  2mo  2675  euind  3685  sbnfc2  4400  uniintsn  4948  eusvnf  5361  copsex2dv  5475  ssopab2dv  5534  ssrel  5767  relssdv  5772  eqrelrdv  5776  eqbrrdv  5777  eqrelrdv2  5779  ssrelrel  5780  iss  6035  iresn0n0  6054  ordelord  6383  suctr  6450  funssres  6581  funun  6583  fununi  6612  fsn  7132  ovg  7581  wemoiso  7973  wemoiso2  7974  oprabexd  7975  frrlem9  8296  omeu  8575  qliftfund  8806  eroveu  8815  fpwwe2lem10  10652  addsrmo  11085  mulsrmo  11086  seqf1o  14109  fi1uzind  14574  brfi1indALT  14577  summo  15805  prodmo  16027  pceu  16942  invfun  17857  initoeu2lem2  18108  psss  18672  psgneu  19634  gsumval3eu  20032  hausflimi  24207  vitalilem3  25839  plyexmo  26544  nosupprefixmo  27934  noinfprefixmo  27935  nosupno  27937  noinfno  27952  bdayons  28539  tglineintmo  28987  frgr3vlem1  30739  3vfriswmgrlem  30743  frgr2wwlk1  30795  pjhthmo  31769  chscl  32108  bnj1379  35326  bnj580  35409  bnj1321  35523  acycgr1v  35715  cvmlift2lem12  35880  satffunlem1lem1  35968  satffunlem2lem1  35970  mclsssvlem  36128  mclsax  36135  mclsind  36136  lineintmo  36724  trer  36922  mbfresfi  38402  unirep  38451  iss2  39079  prter1  39739  islpoldN  42344  ismrcd2  43531  ismrc  43533  tfsconcatb0  44172  mnutrd  45091  truniALT  45351  gen12  45428  sspwtrALT  45631  sspwtrALT2  45632  suctrALT  45635  suctrALT2  45646  trintALT  45690  suctrALTcf  45731  suctrALT3  45733  rlimdmafv  48052  rlimdmafv2  48133  opabresex0d  48160  spr0nelg  48363  sprsymrelfvlem  48377  mofsn  49759  thincmo  50341  functhincfun  50362