Theorem alrimivv 1898

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

Syntax hints:   -> wi 4   A.wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1470  ax-gen 1472  ax-17 1549

This theorem is referenced by:  2ax17  1901  euind  2960  sbnfc2  3154  exmidsssn  4247  exmidel  4250  exmidundif  4251  exmidundifim  4252  ssopab2dv  4326  suctr  4469  eusvnf  4501  ordsuc  4612  ssrel  4764  relssdv  4768  eqrelrdv  4772  eqbrrdv  4773  eqrelrdv2  4775  ssrelrel  4776  iss  5006  funssres  5314  funun  5316  fununi  5343  fsn  5754  ovg  6087  caovimo  6142  oprabexd  6214  qliftfund  6707  eroveu  6715  th3qlem1  6726  exmidfodomrlemim  7311  exmidmotap  7375  addnq0mo  7562  mulnq0mo  7563  ltexprlemdisj  7721  recexprlemdisj  7745  addsrmo  7858  mulsrmo  7859  seqf1og  10668  summodc  11727  prodmodc  11922  pceu  12651  rhmex  13952  limcimo  15170  exmidsbth  16000