Theorem exlimivv 1945

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

Syntax hints:   → wi 4  ∃wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1497  ax-ie2 1542  ax-17 1574

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2839  cgsex4g  2840  opabss  4153  copsexg  4336  elopab  4352  epelg  4387  0nelelxp  4754  elvvuni  4790  optocl  4802  xpsspw  4838  relopabi  4855  relop  4880  reldmm  4950  elreldm  4958  xpmlem  5157  dfco2a  5237  unielrel  5264  oprabid  6050  1stval2  6318  2ndval2  6319  xp1st  6328  xp2nd  6329  poxp  6397  rntpos  6423  dftpos4  6429  tpostpos  6430  tfrlem7  6483  th3qlem2  6807  ener  6953  domtr  6959  unen  6991  xpsnen  7005  mapen  7032  ltdcnq  7617  archnqq  7637  enq0tr  7654  nqnq0pi  7658  nqnq0  7661  nqpnq0nq  7673  nqnq0a  7674  nqnq0m  7675  nq0m0r  7676  nq0a0  7677  nq02m  7685  prarloc  7723  axaddcl  8084  axmulcl  8086  hashfacen  11101  fundm2domnop0  11113  fsumdvdsmul  15734  griedg0ssusgr  16121  bj-inex  16553