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  2641  euind  3692  sbnfc2  4398  uniintsn  4945  eusvnf  5342  copsex2dv  5449  ssopab2dv  5506  ssrel  5737  relssdv  5742  eqrelrdv  5746  eqbrrdv  5747  eqrelrdv2  5749  ssrelrel  5750  iss  5995  iresn0n0  6014  ordelord  6342  suctr  6408  funssres  6544  funun  6546  fununi  6575  fsn  7089  ovg  7534  wemoiso  7931  wemoiso2  7932  oprabexd  7933  frrlem9  8250  omeu  8526  qliftfund  8753  eroveu  8762  fpwwe2lem10  10571  addsrmo  11004  mulsrmo  11005  seqf1o  13986  fi1uzind  14450  brfi1indALT  14453  summo  15660  prodmo  15879  pceu  16794  invfun  17707  initoeu2lem2  17958  psss  18522  psgneu  19421  gsumval3eu  19819  hausflimi  23901  vitalilem3  25545  plyexmo  26255  nosupprefixmo  27646  noinfprefixmo  27647  nosupno  27649  noinfno  27664  bdayon  28214  tglineintmo  28623  frgr3vlem1  30253  3vfriswmgrlem  30257  frgr2wwlk1  30309  pjhthmo  31282  chscl  31621  bnj1379  34814  bnj580  34897  bnj1321  35011  acycgr1v  35130  cvmlift2lem12  35295  satffunlem1lem1  35383  satffunlem2lem1  35385  mclsssvlem  35543  mclsax  35550  mclsind  35551  lineintmo  36139  trer  36298  mbfresfi  37654  unirep  37702  iss2  38320  prter1  38866  islpoldN  41472  ismrcd2  42681  ismrc  42683  tfsconcatb0  43327  mnutrd  44263  truniALT  44525  gen12  44602  sspwtrALT  44805  sspwtrALT2  44806  suctrALT  44809  suctrALT2  44820  trintALT  44864  suctrALTcf  44905  suctrALT3  44907  rlimdmafv  47172  rlimdmafv2  47253  opabresex0d  47280  spr0nelg  47471  sprsymrelfvlem  47485  mofsn  48826  thincmo  49411  functhincfun  49432