Theorem alrimivv 1686

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (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 1685	. 2 |- ( ph -> A. y ps )
3	2	alrimiv 1685	1 |- ( ph -> A. x A. y ps )

Syntax hints:   -> wi 4   A.wal 1367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1591  ax-4 1602  ax-5 1670

This theorem is referenced by:  2ax5  1694  2mo  2360  2moOLD  2361  euind  3146  sbnfc2  3706  uniintsn  4165  eusvnf  4487  ssopab2dv  4617  ordelord  4741  suctr  4802  ssrel  4928  relssdv  4932  eqrelrdv  4936  eqbrrdv  4937  eqrelrdv2  4939  ssrelrel  4940  iss  5154  funssres  5458  funun  5460  fununi  5484  fsn  5881  ovg  6229  wemoiso  6562  wemoiso2  6563  oprabexd  6564  omeu  7024  qliftfund  7186  eroveu  7195  th3qlem1  7206  fpwwe2lem11  8807  seqf1o  11847  brfi1uzind  12219  swrd0  12327  summo  13194  pceu  13913  invfun  14702  psss  15384  psgneu  16012  gsumval3eu  16381  hausflimi  19553  vitalilem3  21090  plyexmo  21779  tglineintmo  23047  pjhthmo  24705  chscl  25044  cvmlift2lem12  27203  prodmo  27449  lineintmo  28188  mbfresfi  28438  trer  28511  unirep  28606  prter1  29024  ismrcd2  29035  ismrc  29037  rlimdmafv  30083  frgra3vlem1  30592  3vfriswmgralem  30596  frg2wot1  30650  2spotdisj  30654  truniALT  31248  gen12  31340  sspwtrALT  31556  sspwtrALT2  31559  suctrALT  31562  suctrALT2  31573  trintALT  31617  suctrALTcf  31658  suctrALT3  31660  bnj1379  31824  bnj580  31906  bnj1321  32018  islpoldN  35129