Theorem exlimivv 1919

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

Syntax hints:   → wi 4  ∃wex 1514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1471  ax-ie2 1516  ax-17 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2807  cgsex4g  2808  opabss  4107  copsexg  4287  elopab  4302  epelg  4335  0nelelxp  4702  elvvuni  4737  optocl  4749  xpsspw  4785  relopabi  4801  relop  4826  elreldm  4902  xpmlem  5100  dfco2a  5180  unielrel  5207  oprabid  5966  1stval2  6231  2ndval2  6232  xp1st  6241  xp2nd  6242  poxp  6308  rntpos  6333  dftpos4  6339  tpostpos  6340  tfrlem7  6393  th3qlem2  6715  ener  6856  domtr  6862  unen  6893  xpsnen  6898  mapen  6925  ltdcnq  7492  archnqq  7512  enq0tr  7529  nqnq0pi  7533  nqnq0  7536  nqpnq0nq  7548  nqnq0a  7549  nqnq0m  7550  nq0m0r  7551  nq0a0  7552  nq02m  7560  prarloc  7598  axaddcl  7959  axmulcl  7961  hashfacen  10962  fsumdvdsmul  15381  bj-inex  15707