Theorem exlimivv 1952

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  cgsex2g  2858  cgsex4g  2859  opabss  4195  copsexg  4384  elopab  4400  epelg  4435  0nelelxp  4803  elvvuni  4839  optocl  4851  xpsspw  4887  relopabi  4905  relop  4930  reldmm  5000  elreldm  5008  xpmlem  5208  dfco2a  5288  unielrel  5315  oprabid  6117  1stval2  6389  2ndval2  6390  xp1st  6399  xp2nd  6400  poxp  6468  rntpos  6528  dftpos4  6534  tpostpos  6535  tfrlem7  6588  th3qlem2  6912  ener  7066  domtr  7072  unen  7105  xpsnen  7119  mapen  7146  ltdcnq  7765  archnqq  7785  enq0tr  7802  nqnq0pi  7806  nqnq0  7809  nqpnq0nq  7821  nqnq0a  7822  nqnq0m  7823  nq0m0r  7824  nq0a0  7825  nq02m  7833  prarloc  7871  axaddcl  8232  axmulcl  8234  hashfacen  11300  fundm2domnop0  11316  fsumdvdsmul  16246  griedg0ssusgr  16658  bj-inex  17099