Theorem alrimivv 1863

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

Syntax hints:   -> wi 4   A.wal 1341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1435  ax-gen 1437  ax-17 1514

This theorem is referenced by:  2ax17  1866  euind  2912  sbnfc2  3104  exmidsssn  4180  exmidel  4183  exmidundif  4184  exmidundifim  4185  ssopab2dv  4255  suctr  4398  eusvnf  4430  ordsuc  4539  ssrel  4691  relssdv  4695  eqrelrdv  4699  eqbrrdv  4700  eqrelrdv2  4702  ssrelrel  4703  iss  4929  funssres  5229  funun  5231  fununi  5255  fsn  5656  ovg  5976  caovimo  6031  oprabexd  6092  qliftfund  6580  eroveu  6588  th3qlem1  6599  exmidfodomrlemim  7153  addnq0mo  7384  mulnq0mo  7385  ltexprlemdisj  7543  recexprlemdisj  7567  addsrmo  7680  mulsrmo  7681  summodc  11320  prodmodc  11515  pceu  12223  limcimo  13234  exmidsbth  13863