Theorem alrimivv 1928

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  2ax5  1937  2mo  2642  euind  3698  sbnfc2  4405  uniintsn  4952  eusvnf  5350  copsex2dv  5457  ssopab2dv  5514  ssrel  5748  ssrelOLD  5749  relssdv  5754  eqrelrdv  5758  eqbrrdv  5759  eqrelrdv2  5761  ssrelrel  5762  iss  6009  iresn0n0  6028  ordelord  6357  suctr  6423  funssres  6563  funun  6565  fununi  6594  fsn  7110  opabresex2d  7445  fvmptopabOLD  7447  ovg  7557  wemoiso  7955  wemoiso2  7956  oprabexd  7957  frrlem9  8276  omeu  8552  qliftfund  8779  eroveu  8788  fpwwe2lem10  10600  addsrmo  11033  mulsrmo  11034  seqf1o  14015  fi1uzind  14479  brfi1indALT  14482  summo  15690  prodmo  15909  pceu  16824  invfun  17733  initoeu2lem2  17984  psss  18546  psgneu  19443  gsumval3eu  19841  hausflimi  23874  vitalilem3  25518  plyexmo  26228  nosupprefixmo  27619  noinfprefixmo  27620  nosupno  27622  noinfno  27637  bdayon  28180  tglineintmo  28576  frgr3vlem1  30209  3vfriswmgrlem  30213  frgr2wwlk1  30265  pjhthmo  31238  chscl  31577  bnj1379  34827  bnj580  34910  bnj1321  35024  acycgr1v  35143  cvmlift2lem12  35308  satffunlem1lem1  35396  satffunlem2lem1  35398  mclsssvlem  35556  mclsax  35563  mclsind  35564  lineintmo  36152  trer  36311  mbfresfi  37667  unirep  37715  iss2  38333  prter1  38879  islpoldN  41485  ismrcd2  42694  ismrc  42696  tfsconcatb0  43340  mnutrd  44276  truniALT  44538  gen12  44615  sspwtrALT  44818  sspwtrALT2  44819  suctrALT  44822  suctrALT2  44833  trintALT  44877  suctrALTcf  44918  suctrALT3  44920  rlimdmafv  47182  rlimdmafv2  47263  opabresex0d  47290  spr0nelg  47481  sprsymrelfvlem  47495  mofsn  48836  thincmo  49421  functhincfun  49442