Theorem alrimivv 1886

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 1885	. 2 |- ( ph -> A. y ps )
3	2	alrimiv 1885	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 1458  ax-gen 1460  ax-17 1537

This theorem is referenced by:  2ax17  1889  euind  2948  sbnfc2  3142  exmidsssn  4232  exmidel  4235  exmidundif  4236  exmidundifim  4237  ssopab2dv  4310  suctr  4453  eusvnf  4485  ordsuc  4596  ssrel  4748  relssdv  4752  eqrelrdv  4756  eqbrrdv  4757  eqrelrdv2  4759  ssrelrel  4760  iss  4989  funssres  5297  funun  5299  fununi  5323  fsn  5731  ovg  6059  caovimo  6114  oprabexd  6181  qliftfund  6674  eroveu  6682  th3qlem1  6693  exmidfodomrlemim  7263  exmidmotap  7323  addnq0mo  7509  mulnq0mo  7510  ltexprlemdisj  7668  recexprlemdisj  7692  addsrmo  7805  mulsrmo  7806  seqf1og  10595  summodc  11529  prodmodc  11724  pceu  12436  rhmex  13656  limcimo  14844  exmidsbth  15584