Theorem alrimivv 1924

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

Syntax hints:   -> wi 4   A.wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1496  ax-gen 1498  ax-17 1575

This theorem is referenced by:  2ax17  1927  euind  3006  sbnfc2  3201  exmidsssn  4317  exmidel  4320  exmidundif  4321  exmidundifim  4322  ssopab2dv  4399  suctr  4544  eusvnf  4576  ordsuc  4687  ssrel  4840  relssdv  4844  eqrelrdv  4848  eqbrrdv  4849  eqrelrdv2  4851  ssrelrel  4852  iss  5086  funssres  5397  funun  5399  fununi  5426  fsn  5851  ovg  6195  caovimo  6250  oprabexd  6322  qliftfund  6854  eroveu  6862  th3qlem1  6873  exmidssfi  7201  exmidfodomrlemim  7506  exmidmotap  7577  addnq0mo  7764  mulnq0mo  7765  ltexprlemdisj  7923  recexprlemdisj  7947  addsrmo  8060  mulsrmo  8061  seqf1og  10887  summodc  12073  prodmodc  12268  pceu  12997  rhmex  14319  limcimo  15547  exmidsbth  16821  gfsumval  16879