Theorem exlimivv 1943

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

Syntax hints:   → wi 4  ∃wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2837  cgsex4g  2838  opabss  4151  copsexg  4334  elopab  4350  epelg  4385  0nelelxp  4752  elvvuni  4788  optocl  4800  xpsspw  4836  relopabi  4853  relop  4878  reldmm  4948  elreldm  4956  xpmlem  5155  dfco2a  5235  unielrel  5262  oprabid  6045  1stval2  6313  2ndval2  6314  xp1st  6323  xp2nd  6324  poxp  6392  rntpos  6418  dftpos4  6424  tpostpos  6425  tfrlem7  6478  th3qlem2  6802  ener  6948  domtr  6954  unen  6986  xpsnen  7000  mapen  7027  ltdcnq  7607  archnqq  7627  enq0tr  7644  nqnq0pi  7648  nqnq0  7651  nqpnq0nq  7663  nqnq0a  7664  nqnq0m  7665  nq0m0r  7666  nq0a0  7667  nq02m  7675  prarloc  7713  axaddcl  8074  axmulcl  8076  hashfacen  11090  fundm2domnop0  11099  fsumdvdsmul  15705  griedg0ssusgr  16090  bj-inex  16438