Theorem alrimivv 1778

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1992 and 19.21v 1790. (Contributed by NM, 31-Jul-1995.)

Hypothesis

Ref	Expression
alrimivv.1	|- ( ph -> ps )

Assertion

Ref	Expression
alrimivv	|- ( ph -> A. x A. y ps )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)

Proof of Theorem alrimivv

Step	Hyp	Ref	Expression
1		alrimivv.1	. . 3 |- ( ph -> ps )
2	1	alrimiv 1777	. 2 |- ( ph -> A. y ps )
3	2	alrimiv 1777	1 |- ( ph -> A. x A. y ps )

Syntax hints:   -> wi 4   A.wal 1446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1673  ax-4 1686  ax-5 1762

This theorem is referenced by:  2ax5  1788  2mo  2381  euind  3193  sbnfc2  3764  uniintsn  4242  eusvnf  4571  ssopab2dv  4703  ssrel  4901  relssdv  4905  eqrelrdv  4909  eqbrrdv  4910  eqrelrdv2  4912  ssrelrel  4913  iss  5130  ordelord  5424  suctr  5485  funssres  5601  funun  5603  fununi  5631  fsn  6046  ovg  6423  wemoiso  6766  wemoiso2  6767  oprabexd  6768  omeu  7273  qliftfund  7436  eroveu  7445  fpwwe2lem11  9052  addsrmo  9484  mulsrmo  9485  seqf1o  12248  fi1uzind  12645  brfi1indALT  12648  summo  13794  prodmo  14001  pceu  14807  invfun  15680  initoeu2lem2  15921  psss  16471  psgneu  17158  gsumval3eu  17549  hausflimi  21006  vitalilem3  22580  plyexmo  23278  tglineintmo  24699  frgra3vlem1  25740  3vfriswmgralem  25744  frg2wot1  25797  2spotdisj  25801  pjhthmo  26967  chscl  27306  bnj1379  29648  bnj580  29730  bnj1321  29842  cvmlift2lem12  30043  mclsssvlem  30206  mclsax  30213  mclsind  30214  lineintmo  30930  trer  30978  mbfresfi  31989  unirep  32041  prter1  32453  islpoldN  35054  ismrcd2  35543  ismrc  35545  truniALT  36903  gen12  36997  sspwtrALT  37207  sspwtrALT2  37216  suctrALT  37219  suctrALT2  37230  trintALT  37275  suctrALTcf  37316  suctrALT3  37318  rlimdmafv  38770  opabresex0d  39123  opabresex2d  39127