Theorem alrimivv 1930

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem is referenced by:  2ax5  1939  2mo  2647  euind  3681  sbnfc2  4390  uniintsn  4939  eusvnf  5336  copsex2dv  5441  ssopab2dv  5498  ssrel  5731  relssdv  5736  eqrelrdv  5740  eqbrrdv  5741  eqrelrdv2  5743  ssrelrel  5744  iss  5993  iresn0n0  6012  ordelord  6338  suctr  6404  funssres  6535  funun  6537  fununi  6566  fsn  7080  ovg  7523  wemoiso  7917  wemoiso2  7918  oprabexd  7919  frrlem9  8236  omeu  8512  qliftfund  8742  eroveu  8751  fpwwe2lem10  10553  addsrmo  10986  mulsrmo  10987  seqf1o  13968  fi1uzind  14432  brfi1indALT  14435  summo  15642  prodmo  15861  pceu  16776  invfun  17690  initoeu2lem2  17941  psss  18505  psgneu  19437  gsumval3eu  19835  hausflimi  23926  vitalilem3  25569  plyexmo  26279  nosupprefixmo  27670  noinfprefixmo  27671  nosupno  27673  noinfno  27688  bdayon  28255  tglineintmo  28695  frgr3vlem1  30329  3vfriswmgrlem  30333  frgr2wwlk1  30385  pjhthmo  31358  chscl  31697  bnj1379  34965  bnj580  35048  bnj1321  35162  acycgr1v  35322  cvmlift2lem12  35487  satffunlem1lem1  35575  satffunlem2lem1  35577  mclsssvlem  35735  mclsax  35742  mclsind  35743  lineintmo  36330  trer  36489  mbfresfi  37836  unirep  37884  iss2  38514  prter1  39174  islpoldN  41779  ismrcd2  42978  ismrc  42980  tfsconcatb0  43623  mnutrd  44558  truniALT  44819  gen12  44896  sspwtrALT  45099  sspwtrALT2  45100  suctrALT  45103  suctrALT2  45114  trintALT  45158  suctrALTcf  45199  suctrALT3  45201  rlimdmafv  47460  rlimdmafv2  47541  opabresex0d  47568  spr0nelg  47759  sprsymrelfvlem  47773  mofsn  49126  thincmo  49710  functhincfun  49731