Theorem exlimivv 1889

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

Syntax hints:   → wi 4  ∃wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1442  ax-ie2 1487  ax-17 1519

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cgsex2g  2766  cgsex4g  2767  opabss  4051  copsexg  4227  elopab  4241  epelg  4273  0nelelxp  4638  elvvuni  4673  optocl  4685  xpsspw  4721  relopabi  4735  relop  4759  elreldm  4835  xpmlem  5029  dfco2a  5109  unielrel  5136  oprabid  5883  1stval2  6132  2ndval2  6133  xp1st  6142  xp2nd  6143  poxp  6209  rntpos  6234  dftpos4  6240  tpostpos  6241  tfrlem7  6294  th3qlem2  6613  ener  6754  domtr  6760  unen  6791  xpsnen  6796  mapen  6821  ltdcnq  7348  archnqq  7368  enq0tr  7385  nqnq0pi  7389  nqnq0  7392  nqpnq0nq  7404  nqnq0a  7405  nqnq0m  7406  nq0m0r  7407  nq0a0  7408  nq02m  7416  prarloc  7454  axaddcl  7815  axmulcl  7817  hashfacen  10760  bj-inex  13904