Theorem alrimivv 1856

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

Syntax hints:   -> wi 4   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem is referenced by:  2ax5  1866  2mo  2551  euind  3393  sbnfc2  4007  uniintsn  4514  eusvnf  4861  ssopab2dv  5004  ssrel  5207  ssrelOLD  5208  relssdv  5212  eqrelrdv  5216  eqbrrdv  5217  eqrelrdv2  5219  ssrelrel  5220  iss  5447  ordelord  5745  suctr  5808  suctrOLD  5809  funssres  5930  funun  5932  fununi  5964  fsn  6402  opabresex2d  6696  fvmptopab  6697  ovg  6799  wemoiso  7153  wemoiso2  7154  oprabexd  7155  omeu  7665  qliftfund  7833  eroveu  7842  fpwwe2lem11  9462  addsrmo  9894  mulsrmo  9895  seqf1o  12842  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  summo  14448  prodmo  14666  pceu  15551  invfun  16424  initoeu2lem2  16665  psss  17214  psgneu  17926  gsumval3eu  18305  hausflimi  21784  vitalilem3  23379  plyexmo  24068  tglineintmo  25537  frgr3vlem1  27137  3vfriswmgrlem  27141  frgr2wwlk1  27193  pjhthmo  28161  chscl  28500  bnj1379  30901  bnj580  30983  bnj1321  31095  cvmlift2lem12  31296  mclsssvlem  31459  mclsax  31466  mclsind  31467  noprefixmo  31848  nosupno  31849  lineintmo  32264  trer  32310  mbfresfi  33456  unirep  33507  iss2  34112  prter1  34164  islpoldN  36773  ismrcd2  37262  ismrc  37264  truniALT  38751  gen12  38843  sspwtrALT  39049  sspwtrALT2  39058  suctrALT  39061  suctrALT2  39072  trintALT  39117  suctrALTcf  39158  suctrALT3  39160  rlimdmafv  41257  opabresex0d  41304  spr0nelg  41726  sprsymrelfvlem  41740