Theorem exlimivv 1869

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

Syntax hints:   → wi 4  ∃wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1426  ax-ie2 1471  ax-17 1507

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cgsex2g  2725  cgsex4g  2726  opabss  4000  copsexg  4174  elopab  4188  epelg  4220  0nelelxp  4576  elvvuni  4611  optocl  4623  xpsspw  4659  relopabi  4673  relop  4697  elreldm  4773  xpmlem  4967  dfco2a  5047  unielrel  5074  oprabid  5811  1stval2  6061  2ndval2  6062  xp1st  6071  xp2nd  6072  poxp  6137  rntpos  6162  dftpos4  6168  tpostpos  6169  tfrlem7  6222  th3qlem2  6540  ener  6681  domtr  6687  unen  6718  xpsnen  6723  mapen  6748  ltdcnq  7229  archnqq  7249  enq0tr  7266  nqnq0pi  7270  nqnq0  7273  nqpnq0nq  7285  nqnq0a  7286  nqnq0m  7287  nq0m0r  7288  nq0a0  7289  nq02m  7297  prarloc  7335  axaddcl  7696  axmulcl  7698  hashfacen  10611  bj-inex  13276