Theorem exlimivv 1948

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  2852  cgsex4g  2853  opabss  4180  copsexg  4366  elopab  4382  epelg  4417  0nelelxp  4785  elvvuni  4821  optocl  4833  xpsspw  4869  relopabi  4887  relop  4912  reldmm  4982  elreldm  4990  xpmlem  5190  dfco2a  5270  unielrel  5297  oprabid  6092  1stval2  6364  2ndval2  6365  xp1st  6374  xp2nd  6375  poxp  6443  rntpos  6503  dftpos4  6509  tpostpos  6510  tfrlem7  6563  th3qlem2  6887  ener  7034  domtr  7040  unen  7073  xpsnen  7087  mapen  7114  ltdcnq  7730  archnqq  7750  enq0tr  7767  nqnq0pi  7771  nqnq0  7774  nqpnq0nq  7786  nqnq0a  7787  nqnq0m  7788  nq0m0r  7789  nq0a0  7790  nq02m  7798  prarloc  7836  axaddcl  8197  axmulcl  8199  hashfacen  11238  fundm2domnop0  11250  fsumdvdsmul  15991  griedg0ssusgr  16378  bj-inex  16819