Theorem alrimivv 1886

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

Syntax hints:   -> wi 4   A.wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1458  ax-gen 1460  ax-17 1537

This theorem is referenced by:  2ax17  1889  euind  2947  sbnfc2  3141  exmidsssn  4231  exmidel  4234  exmidundif  4235  exmidundifim  4236  ssopab2dv  4309  suctr  4452  eusvnf  4484  ordsuc  4595  ssrel  4747  relssdv  4751  eqrelrdv  4755  eqbrrdv  4756  eqrelrdv2  4758  ssrelrel  4759  iss  4988  funssres  5296  funun  5298  fununi  5322  fsn  5730  ovg  6057  caovimo  6112  oprabexd  6179  qliftfund  6672  eroveu  6680  th3qlem1  6691  exmidfodomrlemim  7261  exmidmotap  7321  addnq0mo  7507  mulnq0mo  7508  ltexprlemdisj  7666  recexprlemdisj  7690  addsrmo  7803  mulsrmo  7804  seqf1og  10592  summodc  11526  prodmodc  11721  pceu  12433  rhmex  13653  limcimo  14819  exmidsbth  15514