Theorem exlimivv 1945

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. x E. y ph -> 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 1647	. 2 |- ( E. y ph -> ps )
3	2	exlimiv 1647	1 |- ( E. x E. y ph -> ps )

Syntax hints:   -> wi 4   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2840  cgsex4g  2841  opabss  4158  copsexg  4342  elopab  4358  epelg  4393  0nelelxp  4760  elvvuni  4796  optocl  4808  xpsspw  4844  relopabi  4861  relop  4886  reldmm  4956  elreldm  4964  xpmlem  5164  dfco2a  5244  unielrel  5271  oprabid  6060  1stval2  6327  2ndval2  6328  xp1st  6337  xp2nd  6338  poxp  6406  rntpos  6466  dftpos4  6472  tpostpos  6473  tfrlem7  6526  th3qlem2  6850  ener  6996  domtr  7002  unen  7034  xpsnen  7048  mapen  7075  ltdcnq  7677  archnqq  7697  enq0tr  7714  nqnq0pi  7718  nqnq0  7721  nqpnq0nq  7733  nqnq0a  7734  nqnq0m  7735  nq0m0r  7736  nq0a0  7737  nq02m  7745  prarloc  7783  axaddcl  8144  axmulcl  8146  hashfacen  11163  fundm2domnop0  11175  fsumdvdsmul  15805  griedg0ssusgr  16192  bj-inex  16623