Theorem exlimi 2254

Description: Inference associated with 19.23 2248. See exlimiv 1963 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
exlimi.1	⊢ Ⅎ𝑥𝜓
exlimi.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
exlimi	⊢ (∃𝑥𝜑 → 𝜓)

Proof of Theorem exlimi

Step	Hyp	Ref	Expression
1		exlimi.1	. . 3 ⊢ Ⅎ𝑥𝜓
2	1	19.23 2248	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
3		exlimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	mpgbi 1831	1 ⊢ (∃𝑥𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4  ∃wex 1812  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  equsexv  2303  equs5av  2311  exlimih  2323  equs5aALT  2396  equs5eALT  2397  equsex  2448  exdistrf  2477  equs5a  2487  equs5e  2488  dfmoeu  2561  moanim  2646  euan  2647  moexexlem  2652  2eu6  2682  vtoclef  3525  vtoclgf  3530  vtoclg1f  3531  reusv2lem1  5360  copsexgwOLD  5461  copsexg  5462  rexopabb  5502  ralxpf  5824  dmcossOLD  5958  fv3  6901  opabiota  6965  oprabidw  7449  zfregclOLD  9582  scottexOLD  9927  scott0b  9930  scott0OLD  9931  dfac5lem5  10199  zfcndpow  10694  zfcndreg  10695  zfcndinf  10696  reclem2pr  11126  mreiincl  17759  brabgaf  33193  bnj607  35539  bnj900  35552  exisym1  37192  regsfromsetind  37307  exlimii  37723  bj-exlimmpi  37804  bj-exlimmpbi  37805  bj-exlimmpbir  37806  dihglblem5  42335  eu2ndop1stv  48164  pgind  50779