Theorem alrimivv 1755

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

Syntax hints:   -> wi 4   A.wal 1241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1336  ax-gen 1338  ax-17 1419

This theorem is referenced by:  2ax17  1758  euind  2728  sbnfc2  2906  ssopab2dv  4015  suctr  4158  eusvnf  4185  ordsuc  4287  ssrel  4428  relssdv  4432  eqrelrdv  4436  eqbrrdv  4437  eqrelrdv2  4439  ssrelrel  4440  iss  4654  funssres  4942  funun  4944  fununi  4967  fsn  5335  ovg  5639  caovimo  5694  oprabexd  5754  qliftfund  6189  eroveu  6197  th3qlem1  6208  addnq0mo  6545  mulnq0mo  6546  ltexprlemdisj  6704  recexprlemdisj  6728  addsrmo  6828  mulsrmo  6829