Theorem exlimi 2253

Description: Inference associated with 19.23 2247. 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 2247	. 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  2302  equs5av  2310  exlimih  2322  equs5aALT  2395  equs5eALT  2396  equsex  2447  exdistrf  2476  equs5a  2486  equs5e  2487  dfmoeu  2560  moanim  2645  euan  2646  moexexlem  2651  2eu6  2681  vtoclef  3524  vtoclgf  3529  vtoclg1f  3530  reusv2lem1  5363  copsexgwOLD  5467  copsexg  5468  rexopabb  5506  ralxpf  5826  dmcossOLD  5960  fv3  6896  opabiota  6960  oprabidw  7444  zfregclOLD  9567  scottexOLD  9873  scott0b  9876  scott0OLD  9877  dfac5lem5  10130  zfcndpow  10625  zfcndreg  10626  zfcndinf  10627  reclem2pr  11057  mreiincl  17680  brabgaf  33079  bnj607  35425  bnj900  35438  exisym1  37043  regsfromsetind  37158  exlimii  37574  bj-exlimmpi  37655  bj-exlimmpbi  37656  bj-exlimmpbir  37657  dihglblem5  42171  eu2ndop1stv  48013  pgind  50643