Theorem alrimivv 1951

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

Syntax hints:   → wi 4  ∀wal 1561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem is referenced by:  2ax5  1960  2mo  2678  euind  3690  sbnfc2  4396  uniintsn  4946  eusvnf  5354  copsex2dv  5468  ssopab2dv  5527  ssrel  5760  relssdv  5765  eqrelrdv  5769  eqbrrdv  5770  eqrelrdv2  5772  ssrelrel  5773  iss  6028  iresn0n0  6047  ordelord  6372  suctr  6438  funssres  6569  funun  6571  fununi  6600  fsn  7121  ovg  7565  wemoiso  7958  wemoiso2  7959  oprabexd  7960  frrlem9  8279  omeu  8558  qliftfund  8789  eroveu  8798  fpwwe2lem10  10613  addsrmo  11046  mulsrmo  11047  seqf1o  14070  fi1uzind  14534  brfi1indALT  14537  summo  15758  prodmo  15980  pceu  16896  invfun  17811  initoeu2lem2  18062  psss  18626  psgneu  19567  gsumval3eu  19965  hausflimi  24098  vitalilem3  25730  plyexmo  26435  nosupprefixmo  27822  noinfprefixmo  27823  nosupno  27825  noinfno  27840  bdayons  28427  tglineintmo  28869  frgr3vlem1  30533  3vfriswmgrlem  30537  frgr2wwlk1  30589  pjhthmo  31563  chscl  31902  bnj1379  35135  bnj580  35218  bnj1321  35332  acycgr1v  35512  cvmlift2lem12  35677  satffunlem1lem1  35765  satffunlem2lem1  35767  mclsssvlem  35925  mclsax  35932  mclsind  35933  lineintmo  36520  trer  36689  mbfresfi  38177  unirep  38225  iss2  38855  prter1  39515  islpoldN  42120  ismrcd2  43292  ismrc  43294  tfsconcatb0  43933  mnutrd  44854  truniALT  45115  gen12  45192  sspwtrALT  45395  sspwtrALT2  45396  suctrALT  45399  suctrALT2  45410  trintALT  45454  suctrALTcf  45495  suctrALT3  45497  rlimdmafv  47769  rlimdmafv2  47850  opabresex0d  47877  spr0nelg  48080  sprsymrelfvlem  48094  mofsn  49473  thincmo  50057  functhincfun  50078