Theorem alrimivv 1696

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 1695	. 2 |- ( ph -> A. y ps )
3	2	alrimiv 1695	1 |- ( ph -> A. x A. y ps )

Syntax hints:   -> wi 4   A.wal 1377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem is referenced by:  2ax5  1704  2mo  2382  2moOLD  2383  euind  3290  sbnfc2  3854  uniintsn  4319  eusvnf  4642  ssopab2dv  4776  ordelord  4900  suctr  4961  ssrel  5090  relssdv  5094  eqrelrdv  5098  eqbrrdv  5099  eqrelrdv2  5101  ssrelrel  5102  iss  5320  funssres  5627  funun  5629  fununi  5653  fsn  6058  ovg  6424  wemoiso  6769  wemoiso2  6770  oprabexd  6771  omeu  7234  qliftfund  7397  eroveu  7406  fpwwe2lem11  9017  addsrmo  9449  mulsrmo  9450  seqf1o  12115  brfi1uzind  12497  swrd0  12620  summo  13501  pceu  14228  invfun  15018  psss  15700  psgneu  16334  gsumval3eu  16707  hausflimi  20232  vitalilem3  21770  plyexmo  22459  tglineintmo  23751  frgra3vlem1  24692  3vfriswmgralem  24696  frg2wot1  24750  2spotdisj  24754  pjhthmo  25912  chscl  26251  cvmlift2lem12  28415  prodmo  28661  lineintmo  29400  mbfresfi  29654  trer  29727  unirep  29822  prter1  30240  ismrcd2  30251  ismrc  30253  rlimdmafv  31745  truniALT  32401  gen12  32493  sspwtrALT  32709  sspwtrALT2  32712  suctrALT  32715  suctrALT2  32726  trintALT  32770  suctrALTcf  32811  suctrALT3  32813  bnj1379  32977  bnj580  33059  bnj1321  33171  islpoldN  36290