Theorem alrimivv 1928

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

This proof depends on syntax axioms:   -> wi 4   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1500  ax-gen 1502  ax-17 1579

This theorem is used by:  2ax17  1931  euind  3013  sbnfc2  3208  exmidsssn  4341  exmidel  4344  exmidundif  4345  exmidundifim  4346  ssopab2dv  4423  suctr  4568  eusvnf  4601  ordsuc  4712  ssrel  4865  relssdv  4869  eqrelrdv  4873  eqbrrdv  4874  eqrelrdv2  4876  ssrelrel  4877  iss  5112  funssres  5423  funun  5425  fununi  5452  fsn  5883  ovg  6231  caovimo  6286  oprabexd  6364  qliftfund  6897  eroveu  6905  th3qlem1  6916  exmidssfi  7252  exmidfodomrlemim  7559  exmidmotap  7633  addnq0mo  7820  mulnq0mo  7821  ltexprlemdisj  7979  recexprlemdisj  8003  addsrmo  8116  mulsrmo  8117  seqf1og  10978  summodc  12174  prodmodc  12369  pceu  13102  gsumvalfi  14241  rhmex  14572  limcimo  15908  wexmiddiffi  17266  exmidsbth  17292