Theorem alrimivv 1929

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem is referenced by:  2ax5  1938  2mo  2642  euind  3681  sbnfc2  4387  uniintsn  4933  eusvnf  5328  copsex2dv  5432  ssopab2dv  5489  ssrel  5721  relssdv  5726  eqrelrdv  5730  eqbrrdv  5731  eqrelrdv2  5733  ssrelrel  5734  iss  5981  iresn0n0  6000  ordelord  6324  suctr  6390  funssres  6521  funun  6523  fununi  6552  fsn  7063  ovg  7506  wemoiso  7900  wemoiso2  7901  oprabexd  7902  frrlem9  8219  omeu  8495  qliftfund  8722  eroveu  8731  fpwwe2lem10  10523  addsrmo  10956  mulsrmo  10957  seqf1o  13942  fi1uzind  14406  brfi1indALT  14409  summo  15616  prodmo  15835  pceu  16750  invfun  17663  initoeu2lem2  17914  psss  18478  psgneu  19411  gsumval3eu  19809  hausflimi  23888  vitalilem3  25531  plyexmo  26241  nosupprefixmo  27632  noinfprefixmo  27633  nosupno  27635  noinfno  27650  bdayon  28202  tglineintmo  28613  frgr3vlem1  30243  3vfriswmgrlem  30247  frgr2wwlk1  30299  pjhthmo  31272  chscl  31611  bnj1379  34832  bnj580  34915  bnj1321  35029  acycgr1v  35161  cvmlift2lem12  35326  satffunlem1lem1  35414  satffunlem2lem1  35416  mclsssvlem  35574  mclsax  35581  mclsind  35582  lineintmo  36170  trer  36329  mbfresfi  37685  unirep  37733  iss2  38351  prter1  38897  islpoldN  41502  ismrcd2  42711  ismrc  42713  tfsconcatb0  43356  mnutrd  44292  truniALT  44553  gen12  44630  sspwtrALT  44833  sspwtrALT2  44834  suctrALT  44837  suctrALT2  44848  trintALT  44892  suctrALTcf  44933  suctrALT3  44935  rlimdmafv  47187  rlimdmafv2  47268  opabresex0d  47295  spr0nelg  47486  sprsymrelfvlem  47500  mofsn  48854  thincmo  49439  functhincfun  49460