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  6049  1stval2  6317  2ndval2  6318  xp1st  6327  xp2nd  6328  poxp  6396  rntpos  6422  dftpos4  6428  tpostpos  6429  tfrlem7  6482  th3qlem2  6806  ener  6952  domtr  6958  unen  6990  xpsnen  7004  mapen  7031  ltdcnq  7616  archnqq  7636  enq0tr  7653  nqnq0pi  7657  nqnq0  7660  nqpnq0nq  7672  nqnq0a  7673  nqnq0m  7674  nq0m0r  7675  nq0a0  7676  nq02m  7684  prarloc  7722  axaddcl  8083  axmulcl  8085  hashfacen  11099  fundm2domnop0  11108  fsumdvdsmul  15714  griedg0ssusgr  16101  bj-inex  16502