Theorem exlimivv 1946

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

Syntax hints:   → wi 4  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2850  cgsex4g  2851  opabss  4174  copsexg  4360  elopab  4376  epelg  4411  0nelelxp  4778  elvvuni  4814  optocl  4826  xpsspw  4862  relopabi  4880  relop  4905  reldmm  4975  elreldm  4983  xpmlem  5183  dfco2a  5263  unielrel  5290  oprabid  6082  1stval2  6349  2ndval2  6350  xp1st  6359  xp2nd  6360  poxp  6428  rntpos  6488  dftpos4  6494  tpostpos  6495  tfrlem7  6548  th3qlem2  6872  ener  7019  domtr  7025  unen  7058  xpsnen  7072  mapen  7099  ltdcnq  7712  archnqq  7732  enq0tr  7749  nqnq0pi  7753  nqnq0  7756  nqpnq0nq  7768  nqnq0a  7769  nqnq0m  7770  nq0m0r  7771  nq0a0  7772  nq02m  7780  prarloc  7818  axaddcl  8179  axmulcl  8181  hashfacen  11208  fundm2domnop0  11220  fsumdvdsmul  15859  griedg0ssusgr  16246  bj-inex  16677