Theorem alrimivv 1928

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  2ax5  1937  2mo  2648  euind  3712  sbnfc2  4419  uniintsn  4966  eusvnf  5367  copsex2dv  5474  ssopab2dv  5531  ssrel  5766  ssrelOLD  5767  relssdv  5772  eqrelrdv  5776  eqbrrdv  5777  eqrelrdv2  5779  ssrelrel  5780  iss  6027  iresn0n0  6046  ordelord  6379  suctr  6445  funssres  6585  funun  6587  fununi  6616  fsn  7130  opabresex2d  7465  fvmptopabOLD  7467  ovg  7577  wemoiso  7977  wemoiso2  7978  oprabexd  7979  frrlem9  8298  omeu  8602  qliftfund  8822  eroveu  8831  fpwwe2lem10  10659  addsrmo  11092  mulsrmo  11093  seqf1o  14066  fi1uzind  14530  brfi1indALT  14533  summo  15738  prodmo  15957  pceu  16871  invfun  17782  initoeu2lem2  18033  psss  18595  psgneu  19492  gsumval3eu  19890  hausflimi  23923  vitalilem3  25568  plyexmo  26278  nosupprefixmo  27669  noinfprefixmo  27670  nosupno  27672  noinfno  27687  bdayon  28230  tglineintmo  28626  frgr3vlem1  30259  3vfriswmgrlem  30263  frgr2wwlk1  30315  pjhthmo  31288  chscl  31627  bnj1379  34866  bnj580  34949  bnj1321  35063  acycgr1v  35176  cvmlift2lem12  35341  satffunlem1lem1  35429  satffunlem2lem1  35431  mclsssvlem  35589  mclsax  35596  mclsind  35597  lineintmo  36180  trer  36339  mbfresfi  37695  unirep  37743  iss2  38367  prter1  38902  islpoldN  41508  ismrcd2  42689  ismrc  42691  tfsconcatb0  43335  mnutrd  44271  truniALT  44533  gen12  44610  sspwtrALT  44813  sspwtrALT2  44814  suctrALT  44817  suctrALT2  44828  trintALT  44872  suctrALTcf  44913  suctrALT3  44915  rlimdmafv  47173  rlimdmafv2  47254  opabresex0d  47281  spr0nelg  47457  sprsymrelfvlem  47471  mofsn  48789  thincmo  49281  functhincfun  49302