Theorem alrimivv 1932

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

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  2ax5  1941  2mo  2645  euind  3721  sbnfc2  4437  uniintsn  4992  eusvnf  5391  ssopab2dv  5552  ssrel  5783  ssrelOLD  5784  relssdv  5789  eqrelrdv  5793  eqbrrdv  5794  eqrelrdv2  5796  ssrelrel  5797  iss  6036  iresn0n0  6054  ordelord  6387  suctr  6451  funssres  6593  funun  6595  fununi  6624  fsn  7133  opabresex2d  7462  fvmptopabOLD  7464  ovg  7572  wemoiso  7960  wemoiso2  7961  oprabexd  7962  frrlem9  8279  omeu  8585  qliftfund  8797  eroveu  8806  fpwwe2lem10  10635  addsrmo  11068  mulsrmo  11069  seqf1o  14009  fi1uzind  14458  brfi1indALT  14461  summo  15663  prodmo  15880  pceu  16779  invfun  17711  initoeu2lem2  17965  psss  18533  psgneu  19374  gsumval3eu  19772  hausflimi  23484  vitalilem3  25127  plyexmo  25826  nosupprefixmo  27203  noinfprefixmo  27204  nosupno  27206  noinfno  27221  tglineintmo  27893  frgr3vlem1  29526  3vfriswmgrlem  29530  frgr2wwlk1  29582  pjhthmo  30555  chscl  30894  bnj1379  33841  bnj580  33924  bnj1321  34038  acycgr1v  34140  cvmlift2lem12  34305  satffunlem1lem1  34393  satffunlem2lem1  34395  mclsssvlem  34553  mclsax  34560  mclsind  34561  lineintmo  35129  trer  35201  mbfresfi  36534  unirep  36582  iss2  37213  prter1  37749  islpoldN  40355  ismrcd2  41437  ismrc  41439  tfsconcatb0  42094  mnutrd  43039  truniALT  43302  gen12  43379  sspwtrALT  43583  sspwtrALT2  43584  suctrALT  43587  suctrALT2  43598  trintALT  43642  suctrALTcf  43683  suctrALT3  43685  rlimdmafv  45885  rlimdmafv2  45966  opabresex0d  45993  spr0nelg  46144  sprsymrelfvlem  46158  mofsn  47510  thincmo  47649