Theorem exlimivv 1943

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

Syntax hints:   → wi 4  ∃wex 1538

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2836  cgsex4g  2837  opabss  4147  copsexg  4329  elopab  4345  epelg  4380  0nelelxp  4747  elvvuni  4782  optocl  4794  xpsspw  4830  relopabi  4846  relop  4871  reldmm  4941  elreldm  4949  xpmlem  5148  dfco2a  5228  unielrel  5255  oprabid  6032  1stval2  6299  2ndval2  6300  xp1st  6309  xp2nd  6310  poxp  6376  rntpos  6401  dftpos4  6407  tpostpos  6408  tfrlem7  6461  th3qlem2  6783  ener  6929  domtr  6935  unen  6967  xpsnen  6976  mapen  7003  ltdcnq  7580  archnqq  7600  enq0tr  7617  nqnq0pi  7621  nqnq0  7624  nqpnq0nq  7636  nqnq0a  7637  nqnq0m  7638  nq0m0r  7639  nq0a0  7640  nq02m  7648  prarloc  7686  axaddcl  8047  axmulcl  8049  hashfacen  11053  fundm2domnop0  11062  fsumdvdsmul  15659  bj-inex  16228