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  6896  eroveu  6904  th3qlem1  6915  exmidssfi  7250  exmidfodomrlemim  7559  exmidmotap  7633  addnq0mo  7820  mulnq0mo  7821  ltexprlemdisj  7979  recexprlemdisj  8003  addsrmo  8116  mulsrmo  8117  seqf1og  10979  summodc  12175  prodmodc  12370  pceu  13103  gsumvalfi  14242  rhmex  14573  limcimo  15891  wexmiddiffi  17249  exmidsbth  17275