Theorem alrimivv 1923

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

Syntax hints:   -> wi 4   A.wal 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1495  ax-gen 1497  ax-17 1574

This theorem is referenced by:  2ax17  1926  euind  2993  sbnfc2  3188  exmidsssn  4292  exmidel  4295  exmidundif  4296  exmidundifim  4297  ssopab2dv  4373  suctr  4518  eusvnf  4550  ordsuc  4661  ssrel  4814  relssdv  4818  eqrelrdv  4822  eqbrrdv  4823  eqrelrdv2  4825  ssrelrel  4826  iss  5059  funssres  5369  funun  5371  fununi  5398  fsn  5819  ovg  6160  caovimo  6215  oprabexd  6288  qliftfund  6786  eroveu  6794  th3qlem1  6805  exmidssfi  7130  exmidfodomrlemim  7411  exmidmotap  7479  addnq0mo  7666  mulnq0mo  7667  ltexprlemdisj  7825  recexprlemdisj  7849  addsrmo  7962  mulsrmo  7963  seqf1og  10782  summodc  11943  prodmodc  12138  pceu  12867  rhmex  14170  limcimo  15388  exmidsbth  16628  gfsumval  16680