Theorem alrimivv 1768

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

Syntax hints:   -> wi 4   A.wal 1435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1663  ax-4 1676  ax-5 1752

This theorem is referenced by:  2ax5  1777  2mo  2350  euind  3257  sbnfc2  3826  uniintsn  4293  eusvnf  4619  ssopab2dv  4749  ssrel  4942  relssdv  4946  eqrelrdv  4950  eqbrrdv  4951  eqrelrdv2  4953  ssrelrel  4954  iss  5171  ordelord  5464  suctr  5525  funssres  5641  funun  5643  fununi  5667  fsn  6076  ovg  6449  wemoiso  6792  wemoiso2  6793  oprabexd  6794  omeu  7297  qliftfund  7460  eroveu  7469  fpwwe2lem11  9072  addsrmo  9504  mulsrmo  9505  seqf1o  12260  fi1uzind  12654  brfi1indALT  12657  summo  13782  prodmo  13989  pceu  14795  invfun  15668  initoeu2lem2  15909  psss  16459  psgneu  17146  gsumval3eu  17537  hausflimi  20993  vitalilem3  22566  plyexmo  23264  tglineintmo  24685  frgra3vlem1  25726  3vfriswmgralem  25730  frg2wot1  25783  2spotdisj  25787  pjhthmo  26953  chscl  27292  bnj1379  29650  bnj580  29732  bnj1321  29844  cvmlift2lem12  30045  mclsssvlem  30208  mclsax  30215  mclsind  30216  lineintmo  30929  trer  30977  mbfresfi  31951  unirep  32003  prter1  32419  islpoldN  35021  ismrcd2  35510  ismrc  35512  truniALT  36872  gen12  36968  sspwtrALT  37183  sspwtrALT2  37192  suctrALT  37195  suctrALT2  37206  trintALT  37251  suctrALTcf  37292  suctrALT3  37294  rlimdmafv  38549