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  4303  epelg  4336  0nelelxp  4703  elvvuni  4738  optocl  4750  xpsspw  4786  relopabi  4802  relop  4827  elreldm  4903  xpmlem  5102  dfco2a  5182  unielrel  5209  oprabid  5975  1stval2  6240  2ndval2  6241  xp1st  6250  xp2nd  6251  poxp  6317  rntpos  6342  dftpos4  6348  tpostpos  6349  tfrlem7  6402  th3qlem2  6724  ener  6870  domtr  6876  unen  6907  xpsnen  6915  mapen  6942  ltdcnq  7509  archnqq  7529  enq0tr  7546  nqnq0pi  7550  nqnq0  7553  nqpnq0nq  7565  nqnq0a  7566  nqnq0m  7567  nq0m0r  7568  nq0a0  7569  nq02m  7577  prarloc  7615  axaddcl  7976  axmulcl  7978  hashfacen  10979  fundm2domnop0  10988  fsumdvdsmul  15405  bj-inex  15776