Theorem alrimivv 1847

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

Syntax hints:   -> wi 4   A.wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1423  ax-gen 1425  ax-17 1506

This theorem is referenced by:  2ax17  1850  euind  2871  sbnfc2  3060  exmidsssn  4125  exmidel  4128  exmidundif  4129  exmidundifim  4130  ssopab2dv  4200  suctr  4343  eusvnf  4374  ordsuc  4478  ssrel  4627  relssdv  4631  eqrelrdv  4635  eqbrrdv  4636  eqrelrdv2  4638  ssrelrel  4639  iss  4865  funssres  5165  funun  5167  fununi  5191  fsn  5592  ovg  5909  caovimo  5964  oprabexd  6025  qliftfund  6512  eroveu  6520  th3qlem1  6531  exmidfodomrlemim  7057  addnq0mo  7255  mulnq0mo  7256  ltexprlemdisj  7414  recexprlemdisj  7438  addsrmo  7551  mulsrmo  7552  summodc  11152  prodmodc  11347  limcimo  12803  exmidsbth  13219