Theorem exlimivv 1952

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

This proof depends on syntax axioms:   -> wi 4   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  cgsex2g  2858  cgsex4g  2859  opabss  4196  copsexg  4386  elopab  4402  epelg  4437  0nelelxp  4805  elvvuni  4841  optocl  4853  xpsspw  4889  relopabi  4907  relop  4932  reldmm  5002  elreldm  5010  xpmlem  5211  dfco2a  5291  unielrel  5318  oprabid  6120  1stval2  6393  2ndval2  6394  xp1st  6403  xp2nd  6404  poxp  6472  rntpos  6532  dftpos4  6538  tpostpos  6539  tfrlem7  6592  th3qlem2  6916  ener  7070  domtr  7076  unen  7109  xpsnen  7123  mapen  7150  ltdcnq  7770  archnqq  7790  enq0tr  7807  nqnq0pi  7811  nqnq0  7814  nqpnq0nq  7826  nqnq0a  7827  nqnq0m  7828  nq0m0r  7829  nq0a0  7830  nq02m  7838  prarloc  7876  axaddcl  8237  axmulcl  8239  hashfacen  11306  fundm2domnop0  11322  fsumdvdsmul  16285  griedg0ssusgr  16697  bj-inex  17138  idjudju  17252