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  4196  copsexg  4386  elopab  4402  epelg  4437  0nelelxp  4805  elvvuni  4841  optocl  4853  xpsspw  4889  relopabi  4907  relop  4932  reldmm  5002  elreldm  5010  xpmlem  5211  dfco2a  5291  unielrel  5318  oprabid  6120  1stval2  6393  2ndval2  6394  xp1st  6403  xp2nd  6404  poxp  6472  rntpos  6533  dftpos4  6539  tpostpos  6540  tfrlem7  6593  th3qlem2  6917  ener  7072  domtr  7078  unen  7111  xpsnen  7125  mapen  7152  ltdcnq  7770  archnqq  7790  enq0tr  7807  nqnq0pi  7811  nqnq0  7814  nqpnq0nq  7826  nqnq0a  7827  nqnq0m  7828  nq0m0r  7829  nq0a0  7830  nq02m  7838  prarloc  7876  axaddcl  8237  axmulcl  8239  hashfacen  11305  fundm2domnop0  11321  fsumdvdsmul  16302  griedg0ssusgr  16714  bj-inex  17155  idjudju  17269