Theorem exlimivv 1911

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

Syntax hints:   → wi 4  ∃wex 1506

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2799  cgsex4g  2800  opabss  4098  copsexg  4278  elopab  4293  epelg  4326  0nelelxp  4693  elvvuni  4728  optocl  4740  xpsspw  4776  relopabi  4792  relop  4817  elreldm  4893  xpmlem  5091  dfco2a  5171  unielrel  5198  oprabid  5957  1stval2  6222  2ndval2  6223  xp1st  6232  xp2nd  6233  poxp  6299  rntpos  6324  dftpos4  6330  tpostpos  6331  tfrlem7  6384  th3qlem2  6706  ener  6847  domtr  6853  unen  6884  xpsnen  6889  mapen  6916  ltdcnq  7481  archnqq  7501  enq0tr  7518  nqnq0pi  7522  nqnq0  7525  nqpnq0nq  7537  nqnq0a  7538  nqnq0m  7539  nq0m0r  7540  nq0a0  7541  nq02m  7549  prarloc  7587  axaddcl  7948  axmulcl  7950  hashfacen  10945  fsumdvdsmul  15311  bj-inex  15637