Theorem exlimi 2251

Description: Inference associated with 19.23 2245. See exlimiv 1949 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 2245	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
3		exlimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	mpgbi 1817	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1798  Ⅎwnf 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-nf 1803

This theorem is referenced by:  sbalexOLD  2277  equsexv  2302  equs5av  2310  exlimih  2322  equs5aALT  2396  equs5eALT  2397  equsex  2448  exdistrf  2477  equs5a  2487  equs5e  2488  dfmoeu  2561  moanim  2646  euan  2647  moexexlem  2652  2eu6  2682  vtoclef  3528  vtoclgf  3533  vtoclg1f  3534  reusv2lem1  5352  copsexgwOLD  5456  copsexg  5457  rexopabb  5495  ralxpf  5814  dmcossOLD  5948  fv3  6880  opabiota  6944  oprabidw  7422  zfregclOLD  9537  scottex  9837  scott0  9838  dfac5lem5  10077  zfcndpow  10568  zfcndreg  10569  zfcndinf  10570  reclem2pr  11000  mreiincl  17615  brabgaf  32769  bnj607  35172  bnj900  35185  exisym1  36745  regsfromsetind  36860  exlimii  37277  bj-exlimmpi  37358  bj-exlimmpbi  37359  bj-exlimmpbir  37360  dihglblem5  41883  eu2ndop1stv  47680  pgind  50299