Theorem alrimivv 1927

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem is referenced by:  2ax5  1936  2mo  2647  euind  3729  sbnfc2  4438  uniintsn  4984  eusvnf  5391  copsex2dv  5498  ssopab2dv  5555  ssrel  5791  ssrelOLD  5792  relssdv  5797  eqrelrdv  5801  eqbrrdv  5802  eqrelrdv2  5804  ssrelrel  5805  iss  6052  iresn0n0  6071  ordelord  6405  suctr  6469  funssres  6609  funun  6611  fununi  6640  fsn  7154  opabresex2d  7487  fvmptopabOLD  7489  ovg  7599  wemoiso  7999  wemoiso2  8000  oprabexd  8001  frrlem9  8320  omeu  8624  qliftfund  8844  eroveu  8853  fpwwe2lem10  10681  addsrmo  11114  mulsrmo  11115  seqf1o  14085  fi1uzind  14547  brfi1indALT  14550  summo  15754  prodmo  15973  pceu  16885  invfun  17809  initoeu2lem2  18061  psss  18626  psgneu  19525  gsumval3eu  19923  hausflimi  23989  vitalilem3  25646  plyexmo  26356  nosupprefixmo  27746  noinfprefixmo  27747  nosupno  27749  noinfno  27764  tglineintmo  28651  frgr3vlem1  30293  3vfriswmgrlem  30297  frgr2wwlk1  30349  pjhthmo  31322  chscl  31661  bnj1379  34845  bnj580  34928  bnj1321  35042  acycgr1v  35155  cvmlift2lem12  35320  satffunlem1lem1  35408  satffunlem2lem1  35410  mclsssvlem  35568  mclsax  35575  mclsind  35576  lineintmo  36159  trer  36318  mbfresfi  37674  unirep  37722  iss2  38346  prter1  38881  islpoldN  41487  ismrcd2  42715  ismrc  42717  tfsconcatb0  43362  mnutrd  44304  truniALT  44566  gen12  44643  sspwtrALT  44847  sspwtrALT2  44848  suctrALT  44851  suctrALT2  44862  trintALT  44906  suctrALTcf  44947  suctrALT3  44949  rlimdmafv  47194  rlimdmafv2  47275  opabresex0d  47302  spr0nelg  47468  sprsymrelfvlem  47482  mofsn  48758  thincmo  49102  functhincfun  49123