Theorem alrimivv 1855

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

Syntax hints:   -> wi 4   A.wal 1333

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

This theorem is referenced by:  2ax17  1858  euind  2899  sbnfc2  3091  exmidsssn  4162  exmidel  4165  exmidundif  4166  exmidundifim  4167  ssopab2dv  4237  suctr  4380  eusvnf  4411  ordsuc  4520  ssrel  4671  relssdv  4675  eqrelrdv  4679  eqbrrdv  4680  eqrelrdv2  4682  ssrelrel  4683  iss  4909  funssres  5209  funun  5211  fununi  5235  fsn  5636  ovg  5953  caovimo  6008  oprabexd  6069  qliftfund  6556  eroveu  6564  th3qlem1  6575  exmidfodomrlemim  7119  addnq0mo  7350  mulnq0mo  7351  ltexprlemdisj  7509  recexprlemdisj  7533  addsrmo  7646  mulsrmo  7647  summodc  11262  prodmodc  11457  limcimo  12994  exmidsbth  13558