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  3007  sbnfc2  3202  exmidsssn  4320  exmidel  4323  exmidundif  4324  exmidundifim  4325  ssopab2dv  4402  suctr  4547  eusvnf  4579  ordsuc  4690  ssrel  4843  relssdv  4847  eqrelrdv  4851  eqbrrdv  4852  eqrelrdv2  4854  ssrelrel  4855  iss  5089  funssres  5400  funun  5402  fununi  5429  fsn  5854  ovg  6201  caovimo  6256  oprabexd  6333  qliftfund  6865  eroveu  6873  th3qlem1  6884  exmidssfi  7212  exmidfodomrlemim  7517  exmidmotap  7591  addnq0mo  7778  mulnq0mo  7779  ltexprlemdisj  7937  recexprlemdisj  7961  addsrmo  8074  mulsrmo  8075  seqf1og  10907  summodc  12094  prodmodc  12289  pceu  13018  gfsumval  14102  rhmex  14402  limcimo  15656  exmidsbth  16930