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  2649  euind  3671  sbnfc2  4380  uniintsn  4928  eusvnf  5331  copsex2dv  5444  ssopab2dv  5501  ssrel  5734  relssdv  5739  eqrelrdv  5743  eqbrrdv  5744  eqrelrdv2  5746  ssrelrel  5747  iss  5996  iresn0n0  6015  ordelord  6341  suctr  6407  funssres  6538  funun  6540  fununi  6569  fsn  7084  ovg  7527  wemoiso  7921  wemoiso2  7922  oprabexd  7923  frrlem9  8239  omeu  8515  qliftfund  8745  eroveu  8754  fpwwe2lem10  10558  addsrmo  10991  mulsrmo  10992  seqf1o  14000  fi1uzind  14464  brfi1indALT  14467  summo  15674  prodmo  15896  pceu  16812  invfun  17726  initoeu2lem2  17977  psss  18541  psgneu  19476  gsumval3eu  19874  hausflimi  23959  vitalilem3  25591  plyexmo  26294  nosupprefixmo  27682  noinfprefixmo  27683  nosupno  27685  noinfno  27700  bdayons  28286  tglineintmo  28728  frgr3vlem1  30362  3vfriswmgrlem  30366  frgr2wwlk1  30418  pjhthmo  31392  chscl  31731  bnj1379  34992  bnj580  35075  bnj1321  35189  acycgr1v  35351  cvmlift2lem12  35516  satffunlem1lem1  35604  satffunlem2lem1  35606  mclsssvlem  35764  mclsax  35771  mclsind  35772  lineintmo  36359  trer  36518  mbfresfi  38007  unirep  38055  iss2  38685  prter1  39345  islpoldN  41950  ismrcd2  43151  ismrc  43153  tfsconcatb0  43796  mnutrd  44731  truniALT  44992  gen12  45069  sspwtrALT  45272  sspwtrALT2  45273  suctrALT  45276  suctrALT2  45287  trintALT  45331  suctrALTcf  45372  suctrALT3  45374  rlimdmafv  47643  rlimdmafv2  47724  opabresex0d  47751  spr0nelg  47954  sprsymrelfvlem  47968  mofsn  49337  thincmo  49921  functhincfun  49942