Theorem alrimivv 1889

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 1888	. 2 |- ( ph -> A. y ps )
3	2	alrimiv 1888	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 1461  ax-gen 1463  ax-17 1540

This theorem is referenced by:  2ax17  1892  euind  2951  sbnfc2  3145  exmidsssn  4236  exmidel  4239  exmidundif  4240  exmidundifim  4241  ssopab2dv  4314  suctr  4457  eusvnf  4489  ordsuc  4600  ssrel  4752  relssdv  4756  eqrelrdv  4760  eqbrrdv  4761  eqrelrdv2  4763  ssrelrel  4764  iss  4993  funssres  5301  funun  5303  fununi  5327  fsn  5737  ovg  6066  caovimo  6121  oprabexd  6193  qliftfund  6686  eroveu  6694  th3qlem1  6705  exmidfodomrlemim  7280  exmidmotap  7344  addnq0mo  7531  mulnq0mo  7532  ltexprlemdisj  7690  recexprlemdisj  7714  addsrmo  7827  mulsrmo  7828  seqf1og  10630  summodc  11565  prodmodc  11760  pceu  12489  rhmex  13789  limcimo  14985  exmidsbth  15755