Theorem alrimivv 1797

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

Syntax hints:   -> wi 4   A.wal 1283

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

This theorem is referenced by:  2ax17  1800  euind  2780  sbnfc2  2963  ssopab2dv  4041  suctr  4184  eusvnf  4211  ordsuc  4314  ssrel  4454  relssdv  4458  eqrelrdv  4462  eqbrrdv  4463  eqrelrdv2  4465  ssrelrel  4466  iss  4684  funssres  4972  funun  4974  fununi  4998  fsn  5367  ovg  5670  caovimo  5725  oprabexd  5785  qliftfund  6255  eroveu  6263  th3qlem1  6274  addnq0mo  6699  mulnq0mo  6700  ltexprlemdisj  6858  recexprlemdisj  6882  addsrmo  6982  mulsrmo  6983