Theorem exlimi 2256

Description: Inference associated with 19.23 2250. 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 2250	. 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 2216

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

This theorem is used by:  equsexv  2306  equs5av  2314  exlimih  2326  equs5aALT  2400  equs5eALT  2401  equsex  2452  exdistrf  2481  equs5a  2491  equs5e  2492  dfmoeu  2565  moanim  2650  euan  2651  moexexlem  2656  2eu6  2686  vtoclef  3531  vtoclgf  3536  vtoclg1f  3537  reusv2lem1  5371  copsexgwOLD  5475  copsexg  5476  rexopabb  5514  ralxpf  5834  dmcossOLD  5968  fv3  6903  opabiota  6967  oprabidw  7447  zfregclOLD  9560  scottexOLD  9866  scott0b  9869  scott0OLD  9870  dfac5lem5  10123  zfcndpow  10612  zfcndreg  10613  zfcndinf  10614  reclem2pr  11044  mreiincl  17665  brabgaf  32980  bnj607  35328  bnj900  35341  exisym1  36968  regsfromsetind  37083  exlimii  37499  bj-exlimmpi  37580  bj-exlimmpbi  37581  bj-exlimmpbir  37582  dihglblem5  42105  eu2ndop1stv  47895  pgind  50528