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  7483  archnqq  7503  enq0tr  7520  nqnq0pi  7524  nqnq0  7527  nqpnq0nq  7539  nqnq0a  7540  nqnq0m  7541  nq0m0r  7542  nq0a0  7543  nq02m  7551  prarloc  7589  axaddcl  7950  axmulcl  7952  hashfacen  10947  fsumdvdsmul  15335  bj-inex  15661