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  4097  copsexg  4277  elopab  4292  epelg  4325  0nelelxp  4692  elvvuni  4727  optocl  4739  xpsspw  4775  relopabi  4791  relop  4816  elreldm  4892  xpmlem  5090  dfco2a  5170  unielrel  5197  oprabid  5954  1stval2  6213  2ndval2  6214  xp1st  6223  xp2nd  6224  poxp  6290  rntpos  6315  dftpos4  6321  tpostpos  6322  tfrlem7  6375  th3qlem2  6697  ener  6838  domtr  6844  unen  6875  xpsnen  6880  mapen  6907  ltdcnq  7464  archnqq  7484  enq0tr  7501  nqnq0pi  7505  nqnq0  7508  nqpnq0nq  7520  nqnq0a  7521  nqnq0m  7522  nq0m0r  7523  nq0a0  7524  nq02m  7532  prarloc  7570  axaddcl  7931  axmulcl  7933  hashfacen  10928  fsumdvdsmul  15227  bj-inex  15553