Theorem alrimivv 1961

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1828  ax-4 1842  ax-5 1943

This theorem is used by:  2ax5  1970  2mo  2673  euind  3682  sbnfc2  4397  uniintsn  4945  eusvnf  5354  copsex2dv  5464  ssopab2dv  5523  ssrel  5756  relssdv  5761  eqrelrdv  5765  eqbrrdv  5766  eqrelrdv2  5768  ssrelrel  5769  iss  6026  iresn0n0  6045  ordelord  6374  suctr  6441  funssres  6573  funun  6575  fununi  6604  fsn  7125  ovg  7574  wemoiso  7969  wemoiso2  7970  oprabexd  7971  frrlem9  8291  omeu  8572  qliftfund  8803  eroveu  8812  fpwwe2lem10  10682  addsrmo  11115  mulsrmo  11116  seqf1o  14140  fi1uzind  14605  brfi1indALT  14608  summo  15836  prodmo  16056  pceu  16971  invfun  17886  initoeu2lem2  18137  psss  18701  psgneu  19667  gsumval3eu  20065  hausflimi  24246  vitalilem3  25878  plyexmo  26585  nosupprefixmo  27976  noinfprefixmo  27977  nosupno  27979  noinfno  27994  bdayons  28581  tglineintmo  29029  frgr3vlem1  30793  3vfriswmgrlem  30797  frgr2wwlk1  30849  pjhthmo  31823  chscl  32162  bnj1379  35380  bnj580  35463  bnj1321  35577  acycgr1v  35829  cvmlift2lem12  35994  satffunlem1lem1  36082  satffunlem2lem1  36084  mclsssvlem  36242  mclsax  36249  mclsind  36250  lineintmo  36838  trer  37020  mbfresfi  38498  unirep  38562  iss2  39190  prter1  39850  islpoldN  42455  ismrcd2  43642  ismrc  43644  tfsconcatb0  44283  mnutrd  45202  truniALT  45462  gen12  45539  sspwtrALT  45742  sspwtrALT2  45743  suctrALT  45746  suctrALT2  45757  trintALT  45801  suctrALTcf  45842  suctrALT3  45844  rlimdmafv  48163  rlimdmafv2  48244  opabresex0d  48271  spr0nelg  48474  sprsymrelfvlem  48488  mofsn  49870  thincmo  50452  functhincfun  50473