Theorem exlimivv 1945

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  2840  cgsex4g  2841  opabss  4158  copsexg  4342  elopab  4358  epelg  4393  0nelelxp  4760  elvvuni  4796  optocl  4808  xpsspw  4844  relopabi  4861  relop  4886  reldmm  4956  elreldm  4964  xpmlem  5164  dfco2a  5244  unielrel  5271  oprabid  6060  1stval2  6327  2ndval2  6328  xp1st  6337  xp2nd  6338  poxp  6406  rntpos  6466  dftpos4  6472  tpostpos  6473  tfrlem7  6526  th3qlem2  6850  ener  6996  domtr  7002  unen  7034  xpsnen  7048  mapen  7075  ltdcnq  7660  archnqq  7680  enq0tr  7697  nqnq0pi  7701  nqnq0  7704  nqpnq0nq  7716  nqnq0a  7717  nqnq0m  7718  nq0m0r  7719  nq0a0  7720  nq02m  7728  prarloc  7766  axaddcl  8127  axmulcl  8129  hashfacen  11146  fundm2domnop0  11158  fsumdvdsmul  15788  griedg0ssusgr  16175  bj-inex  16606