Theorem alrimivv 1930

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2215 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  2648  euind  3670  sbnfc2  4379  uniintsn  4927  eusvnf  5334  copsex2dv  5448  ssopab2dv  5506  ssrel  5739  relssdv  5744  eqrelrdv  5748  eqbrrdv  5749  eqrelrdv2  5751  ssrelrel  5752  iss  6000  iresn0n0  6019  ordelord  6345  suctr  6411  funssres  6542  funun  6544  fununi  6573  fsn  7088  ovg  7532  wemoiso  7926  wemoiso2  7927  oprabexd  7928  frrlem9  8244  omeu  8520  qliftfund  8750  eroveu  8759  fpwwe2lem10  10563  addsrmo  10996  mulsrmo  10997  seqf1o  14005  fi1uzind  14469  brfi1indALT  14472  summo  15679  prodmo  15901  pceu  16817  invfun  17731  initoeu2lem2  17982  psss  18546  psgneu  19481  gsumval3eu  19879  hausflimi  23945  vitalilem3  25577  plyexmo  26279  nosupprefixmo  27664  noinfprefixmo  27665  nosupno  27667  noinfno  27682  bdayons  28268  tglineintmo  28710  frgr3vlem1  30343  3vfriswmgrlem  30347  frgr2wwlk1  30399  pjhthmo  31373  chscl  31712  bnj1379  34972  bnj580  35055  bnj1321  35169  acycgr1v  35331  cvmlift2lem12  35496  satffunlem1lem1  35584  satffunlem2lem1  35586  mclsssvlem  35744  mclsax  35751  mclsind  35752  lineintmo  36339  trer  36498  mbfresfi  37987  unirep  38035  iss2  38665  prter1  39325  islpoldN  41930  ismrcd2  43131  ismrc  43133  tfsconcatb0  43772  mnutrd  44707  truniALT  44968  gen12  45045  sspwtrALT  45248  sspwtrALT2  45249  suctrALT  45252  suctrALT2  45263  trintALT  45307  suctrALTcf  45348  suctrALT3  45350  rlimdmafv  47625  rlimdmafv2  47706  opabresex0d  47733  spr0nelg  47936  sprsymrelfvlem  47950  mofsn  49319  thincmo  49903  functhincfun  49924