Theorem exlimivv 1817

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

Syntax hints:   → wi 4  ∃wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1378  ax-ie2 1423  ax-17 1459

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  cgsex2g  2635  cgsex4g  2636  opabss  3842  copsexg  3999  elopab  4013  epelg  4045  0nelelxp  4391  elvvuni  4422  optocl  4434  xpsspw  4468  relopabi  4481  relop  4504  elreldm  4578  xpmlem  4764  dfco2a  4841  unielrel  4865  oprabid  5557  1stval2  5802  2ndval2  5803  xp1st  5812  xp2nd  5813  poxp  5873  rntpos  5895  dftpos4  5901  tpostpos  5902  tfrlem7  5956  th3qlem2  6232  ener  6282  domtr  6288  unen  6316  xpsnen  6318  ltdcnq  6587  archnqq  6607  enq0tr  6624  nqnq0pi  6628  nqnq0  6631  nqpnq0nq  6643  nqnq0a  6644  nqnq0m  6645  nq0m0r  6646  nq0a0  6647  nq02m  6655  prarloc  6693  axaddcl  7032  axmulcl  7034  bj-inex  10698