Theorem alrimivv 1931

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem is referenced by:  2ax5  1940  2mo  2650  euind  3659  sbnfc2  4370  uniintsn  4918  eusvnf  5315  ssopab2dv  5464  ssrel  5693  ssrelOLD  5694  relssdv  5698  eqrelrdv  5702  eqbrrdv  5703  eqrelrdv2  5705  ssrelrel  5706  iss  5943  iresn0n0  5963  ordelord  6288  suctr  6349  funssres  6478  funun  6480  fununi  6509  fsn  7007  opabresex2d  7328  fvmptopabOLD  7330  ovg  7437  wemoiso  7816  wemoiso2  7817  oprabexd  7818  frrlem9  8110  omeu  8416  qliftfund  8592  eroveu  8601  fpwwe2lem10  10396  addsrmo  10829  mulsrmo  10830  seqf1o  13764  fi1uzind  14211  brfi1indALT  14214  summo  15429  prodmo  15646  pceu  16547  invfun  17476  initoeu2lem2  17730  psss  18298  psgneu  19114  gsumval3eu  19505  hausflimi  23131  vitalilem3  24774  plyexmo  25473  tglineintmo  27003  frgr3vlem1  28637  3vfriswmgrlem  28641  frgr2wwlk1  28693  pjhthmo  29664  chscl  30003  bnj1379  32810  bnj580  32893  bnj1321  33007  acycgr1v  33111  cvmlift2lem12  33276  satffunlem1lem1  33364  satffunlem2lem1  33366  mclsssvlem  33524  mclsax  33531  mclsind  33532  nosupprefixmo  33903  noinfprefixmo  33904  nosupno  33906  noinfno  33921  lineintmo  34459  trer  34505  mbfresfi  35823  unirep  35871  iss2  36479  prter1  36893  islpoldN  39498  ismrcd2  40521  ismrc  40523  mnutrd  41898  truniALT  42161  gen12  42238  sspwtrALT  42442  sspwtrALT2  42443  suctrALT  42446  suctrALT2  42457  trintALT  42501  suctrALTcf  42542  suctrALT3  42544  rlimdmafv  44669  rlimdmafv2  44750  opabresex0d  44777  spr0nelg  44928  sprsymrelfvlem  44942  mofsn  46171  thincmo  46310