Theorem alrimivv 1936

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

Syntax hints:   → wi 4  ∀wal 1546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem is referenced by:  2ax5  1945  2mo  2654  euind  3667  sbnfc2  4370  uniintsn  4918  eusvnf  5324  copsex2dv  5438  ssopab2dv  5496  ssrel  5729  relssdv  5734  eqrelrdv  5738  eqbrrdv  5739  eqrelrdv2  5741  ssrelrel  5742  iss  5994  iresn0n0  6013  ordelord  6336  suctr  6402  funssres  6533  funun  6535  fununi  6564  fsn  7081  ovg  7525  wemoiso  7919  wemoiso2  7920  oprabexd  7921  frrlem9  8238  omeu  8514  qliftfund  8744  eroveu  8753  fpwwe2lem10  10558  addsrmo  10991  mulsrmo  10992  seqf1o  14000  fi1uzind  14464  brfi1indALT  14467  summo  15674  prodmo  15896  pceu  16812  invfun  17726  initoeu2lem2  17977  psss  18541  psgneu  19476  gsumval3eu  19874  hausflimi  23967  vitalilem3  25599  plyexmo  26301  nosupprefixmo  27686  noinfprefixmo  27687  nosupno  27689  noinfno  27704  bdayons  28290  tglineintmo  28732  frgr3vlem1  30365  3vfriswmgrlem  30369  frgr2wwlk1  30421  pjhthmo  31395  chscl  31734  bnj1379  35027  bnj580  35110  bnj1321  35224  acycgr1v  35392  cvmlift2lem12  35557  satffunlem1lem1  35645  satffunlem2lem1  35647  mclsssvlem  35805  mclsax  35812  mclsind  35813  lineintmo  36400  trer  36559  mbfresfi  38048  unirep  38096  iss2  38726  prter1  39386  islpoldN  41991  ismrcd2  43163  ismrc  43165  tfsconcatb0  43804  mnutrd  44739  truniALT  45000  gen12  45077  sspwtrALT  45280  sspwtrALT2  45281  suctrALT  45284  suctrALT2  45295  trintALT  45339  suctrALTcf  45380  suctrALT3  45382  rlimdmafv  47654  rlimdmafv2  47735  opabresex0d  47762  spr0nelg  47965  sprsymrelfvlem  47979  mofsn  49348  thincmo  49932  functhincfun  49953