Theorem exlimivv 1896

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

Syntax hints:   → wi 4  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2774  cgsex4g  2775  opabss  4068  copsexg  4245  elopab  4259  epelg  4291  0nelelxp  4656  elvvuni  4691  optocl  4703  xpsspw  4739  relopabi  4753  relop  4778  elreldm  4854  xpmlem  5050  dfco2a  5130  unielrel  5157  oprabid  5907  1stval2  6156  2ndval2  6157  xp1st  6166  xp2nd  6167  poxp  6233  rntpos  6258  dftpos4  6264  tpostpos  6265  tfrlem7  6318  th3qlem2  6638  ener  6779  domtr  6785  unen  6816  xpsnen  6821  mapen  6846  ltdcnq  7396  archnqq  7416  enq0tr  7433  nqnq0pi  7437  nqnq0  7440  nqpnq0nq  7452  nqnq0a  7453  nqnq0m  7454  nq0m0r  7455  nq0a0  7456  nq02m  7464  prarloc  7502  axaddcl  7863  axmulcl  7865  hashfacen  10816  bj-inex  14662