Theorem alrimivv 1868

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

Syntax hints:   -> wi 4   A.wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1440  ax-gen 1442  ax-17 1519

This theorem is referenced by:  2ax17  1871  euind  2917  sbnfc2  3109  exmidsssn  4188  exmidel  4191  exmidundif  4192  exmidundifim  4193  ssopab2dv  4263  suctr  4406  eusvnf  4438  ordsuc  4547  ssrel  4699  relssdv  4703  eqrelrdv  4707  eqbrrdv  4708  eqrelrdv2  4710  ssrelrel  4711  iss  4937  funssres  5240  funun  5242  fununi  5266  fsn  5668  ovg  5991  caovimo  6046  oprabexd  6106  qliftfund  6596  eroveu  6604  th3qlem1  6615  exmidfodomrlemim  7178  addnq0mo  7409  mulnq0mo  7410  ltexprlemdisj  7568  recexprlemdisj  7592  addsrmo  7705  mulsrmo  7706  summodc  11346  prodmodc  11541  pceu  12249  limcimo  13428  exmidsbth  14056