Theorem alrimivv 1725

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1910 and 19.21v 1734. (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 1724	. 2 |- ( ph -> A. y ps )
3	2	alrimiv 1724	1 |- ( ph -> A. x A. y ps )

Syntax hints:   -> wi 4   A.wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1623  ax-4 1636  ax-5 1709

This theorem is referenced by:  2ax5  1733  2mo  2370  2moOLD  2371  euind  3283  sbnfc2  3846  uniintsn  4309  eusvnf  4632  ssopab2dv  4765  ordelord  4889  suctr  4950  ssrel  5079  relssdv  5083  eqrelrdv  5087  eqbrrdv  5088  eqrelrdv2  5090  ssrelrel  5091  iss  5309  funssres  5610  funun  5612  fununi  5636  fsn  6045  ovg  6414  wemoiso  6758  wemoiso2  6759  oprabexd  6760  omeu  7226  qliftfund  7389  eroveu  7398  fpwwe2lem11  9007  addsrmo  9439  mulsrmo  9440  seqf1o  12130  brfi1uzind  12516  summo  13621  prodmo  13825  pceu  14454  invfun  15252  initoeu2lem2  15493  psss  16043  psgneu  16730  gsumval3eu  17106  hausflimi  20647  vitalilem3  22185  plyexmo  22875  tglineintmo  24223  frgra3vlem1  25202  3vfriswmgralem  25206  frg2wot1  25259  2spotdisj  25263  pjhthmo  26418  chscl  26757  cvmlift2lem12  29023  mclsssvlem  29186  mclsax  29193  mclsind  29194  lineintmo  30035  mbfresfi  30301  trer  30374  unirep  30443  prter1  30860  ismrcd2  30871  ismrc  30873  rlimdmafv  32501  truniALT  33702  gen12  33798  sspwtrALT  34014  sspwtrALT2  34023  suctrALT  34026  suctrALT2  34037  trintALT  34082  suctrALTcf  34123  suctrALT3  34125  bnj1379  34290  bnj580  34372  bnj1321  34484  islpoldN  37608