Theorem alrimivv 1930

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem is referenced by:  2ax5  1939  2mo  2649  euind  3683  sbnfc2  4392  uniintsn  4941  eusvnf  5338  copsex2dv  5443  ssopab2dv  5500  ssrel  5733  relssdv  5738  eqrelrdv  5742  eqbrrdv  5743  eqrelrdv2  5745  ssrelrel  5746  iss  5995  iresn0n0  6014  ordelord  6340  suctr  6406  funssres  6537  funun  6539  fununi  6568  fsn  7082  ovg  7525  wemoiso  7919  wemoiso2  7920  oprabexd  7921  frrlem9  8238  omeu  8514  qliftfund  8744  eroveu  8753  fpwwe2lem10  10555  addsrmo  10988  mulsrmo  10989  seqf1o  13970  fi1uzind  14434  brfi1indALT  14437  summo  15644  prodmo  15863  pceu  16778  invfun  17692  initoeu2lem2  17943  psss  18507  psgneu  19439  gsumval3eu  19837  hausflimi  23928  vitalilem3  25571  plyexmo  26281  nosupprefixmo  27672  noinfprefixmo  27673  nosupno  27675  noinfno  27690  bdayons  28276  tglineintmo  28718  frgr3vlem1  30352  3vfriswmgrlem  30356  frgr2wwlk1  30408  pjhthmo  31381  chscl  31720  bnj1379  34988  bnj580  35071  bnj1321  35185  acycgr1v  35345  cvmlift2lem12  35510  satffunlem1lem1  35598  satffunlem2lem1  35600  mclsssvlem  35758  mclsax  35765  mclsind  35766  lineintmo  36353  trer  36512  mbfresfi  37869  unirep  37917  iss2  38547  prter1  39207  islpoldN  41812  ismrcd2  43008  ismrc  43010  tfsconcatb0  43653  mnutrd  44588  truniALT  44849  gen12  44926  sspwtrALT  45129  sspwtrALT2  45130  suctrALT  45133  suctrALT2  45144  trintALT  45188  suctrALTcf  45229  suctrALT3  45231  rlimdmafv  47490  rlimdmafv2  47571  opabresex0d  47598  spr0nelg  47789  sprsymrelfvlem  47803  mofsn  49156  thincmo  49740  functhincfun  49761