Theorem exlimi 2253

Description: Inference associated with 19.23 2247. See exlimiv 1962 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 1830	1 ⊢ (∃𝑥𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4  ∃wex 1811  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

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  5359  copsexgwOLD  5460  copsexg  5461  rexopabb  5501  ralxpf  5823  dmcossOLD  5957  fv3  6904  opabiota  6968  oprabidw  7452  zfregclOLD  9593  scottexOLD  9938  scott0b  9941  scott0OLD  9942  dfac5lem5  10210  zfcndpow  10705  zfcndreg  10706  zfcndinf  10707  reclem2pr  11137  mreiincl  17772  brabgaf  33248  bnj607  35593  bnj900  35606  exisym1  37305  regsfromsetind  37420  exlimii  37836  bj-exlimmpi  37917  bj-exlimmpbi  37918  bj-exlimmpbir  37919  dihglblem5  42449  eu2ndop1stv  48289  pgind  50979