Theorem exlimivv 1943

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

Hypothesis

Ref	Expression
exlimivv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
exlimivv	⊢ (∃𝑥∃𝑦𝜑 → 𝜓)

Distinct variable groups:   𝜓,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem exlimivv

Step	Hyp	Ref	Expression
1		exlimivv.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	exlimiv 1644	. 2 ⊢ (∃𝑦𝜑 → 𝜓)
3	2	exlimiv 1644	1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2836  cgsex4g  2837  opabss  4148  copsexg  4330  elopab  4346  epelg  4381  0nelelxp  4748  elvvuni  4783  optocl  4795  xpsspw  4831  relopabi  4847  relop  4872  reldmm  4942  elreldm  4950  xpmlem  5149  dfco2a  5229  unielrel  5256  oprabid  6039  1stval2  6307  2ndval2  6308  xp1st  6317  xp2nd  6318  poxp  6384  rntpos  6409  dftpos4  6415  tpostpos  6416  tfrlem7  6469  th3qlem2  6793  ener  6939  domtr  6945  unen  6977  xpsnen  6988  mapen  7015  ltdcnq  7595  archnqq  7615  enq0tr  7632  nqnq0pi  7636  nqnq0  7639  nqpnq0nq  7651  nqnq0a  7652  nqnq0m  7653  nq0m0r  7654  nq0a0  7655  nq02m  7663  prarloc  7701  axaddcl  8062  axmulcl  8064  hashfacen  11071  fundm2domnop0  11080  fsumdvdsmul  15680  bj-inex  16325