Theorem exlimivv 1908

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 1609	. 2 ⊢ (∃𝑦𝜑 → 𝜓)
3	2	exlimiv 1609	1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1460  ax-ie2 1505  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2796  cgsex4g  2797  opabss  4093  copsexg  4273  elopab  4288  epelg  4321  0nelelxp  4688  elvvuni  4723  optocl  4735  xpsspw  4771  relopabi  4787  relop  4812  elreldm  4888  xpmlem  5086  dfco2a  5166  unielrel  5193  oprabid  5950  1stval2  6208  2ndval2  6209  xp1st  6218  xp2nd  6219  poxp  6285  rntpos  6310  dftpos4  6316  tpostpos  6317  tfrlem7  6370  th3qlem2  6692  ener  6833  domtr  6839  unen  6870  xpsnen  6875  mapen  6902  ltdcnq  7457  archnqq  7477  enq0tr  7494  nqnq0pi  7498  nqnq0  7501  nqpnq0nq  7513  nqnq0a  7514  nqnq0m  7515  nq0m0r  7516  nq0a0  7517  nq02m  7525  prarloc  7563  axaddcl  7924  axmulcl  7926  hashfacen  10907  bj-inex  15399