Theorem exlimivv 1635

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)

Hypothesis

Ref	Expression
exlimivv.1	|- (ph -> ps)

Assertion

Ref	Expression
exlimivv	|- (E.xE.yph -> ps)

Distinct variable groups:   ps,x   ps,y

Allowed substitution hints:   ph(x,y)

Proof of Theorem exlimivv

Step	Hyp	Ref	Expression
1		exlimivv.1	. . 3 |- (ph -> ps)
2	1	exlimiv 1634	. 2 |- (E.yph -> ps)
3	2	exlimiv 1634	1 |- (E.xE.yph -> ps)

Syntax hints:   -> wi 4  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  2mo  2282  cgsex2g  2892  cgsex4g  2893  elxpk  4197  opkabssvvk  4209  sikss1c1c  4268  ins2kss  4280  ins3kss  4281  cokrelk  4285  pw1equn  4332  pw1eqadj  4333  copsexg  4608  elopab  4697  brsi  4762  optocl  4839  xpnz  5046  dfco2a  5082  dfxp2  5114  1stfo  5506  2ndfo  5507  brswap  5510  oprabid  5551  brtxp  5784  txpcofun  5804  pw1fnf1o  5856  entr  6039  unen  6049  xpen  6056  xpassen  6058  mucnc  6132  muccl  6133  muccom  6135  mucass  6136  ncaddccl  6145  ncdisjeq  6149  tcdi  6165  elce  6176  ce0addcnnul  6180  cenc  6182  sbthlem3  6206  dflec3  6222  nclenc  6223  lenc  6224  tc11  6229  taddc  6230  letc  6232  ce2le  6234  muc0or  6253  frecxp  6315