Theorem alrimivv 1767

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1962 and 19.21v 1778. (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 1766	. 2 |- ( ph -> A. y ps )
3	2	alrimiv 1766	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 1665  ax-4 1678  ax-5 1751

This theorem is referenced by:  2ax5  1776  2mo  2351  2moOLD  2352  euind  3264  sbnfc2  3830  uniintsn  4296  eusvnf  4620  ssopab2dv  4750  ssrel  4943  relssdv  4947  eqrelrdv  4951  eqbrrdv  4952  eqrelrdv2  4954  ssrelrel  4955  iss  5172  ordelord  5464  suctr  5525  funssres  5641  funun  5643  fununi  5667  fsn  6076  ovg  6449  wemoiso  6792  wemoiso2  6793  oprabexd  6794  omeu  7294  qliftfund  7457  eroveu  7466  fpwwe2lem11  9064  addsrmo  9496  mulsrmo  9497  seqf1o  12251  brfi1uzind  12641  summo  13761  prodmo  13968  pceu  14759  invfun  15620  initoeu2lem2  15861  psss  16411  psgneu  17098  gsumval3eu  17473  hausflimi  20926  vitalilem3  22445  plyexmo  23134  tglineintmo  24546  frgra3vlem1  25573  3vfriswmgralem  25577  frg2wot1  25630  2spotdisj  25634  pjhthmo  26790  chscl  27129  bnj1379  29430  bnj580  29512  bnj1321  29624  cvmlift2lem12  29825  mclsssvlem  29988  mclsax  29995  mclsind  29996  lineintmo  30709  trer  30757  mbfresfi  31691  unirep  31743  prter1  32159  islpoldN  34761  ismrcd2  35250  ismrc  35252  truniALT  36539  gen12  36635  sspwtrALT  36850  sspwtrALT2  36859  suctrALT  36862  suctrALT2  36873  trintALT  36918  suctrALTcf  36959  suctrALT3  36961  rlimdmafv  38069