Theorem exlimi 2257

Description: Inference associated with 19.23 2251. See exlimiv 1965 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 2251	. 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 1945  ax-6 2002  ax-7 2043  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  2398  equs5eALT  2399  equsex  2450  exdistrf  2479  equs5a  2489  equs5e  2490  dfmoeu  2563  moanim  2648  euan  2649  moexexlem  2654  2eu6  2684  vtoclef  3528  vtoclgf  3533  vtoclg1f  3534  reusv2lem1  5367  copsexgwOLD  5468  copsexg  5469  rexopabb  5509  ralxpf  5834  dmcossOLD  5970  fv3  6934  opabiota  6998  oprabidw  7482  zfregclOLD  9626  scottexOLD  9971  scott0b  9974  scott0OLD  9975  dfac5lem5  10245  zfcndpow  10740  zfcndreg  10741  zfcndinf  10742  reclem2pr  11172  mreiincl  17816  brabgaf  33298  bnj607  35657  bnj900  35670  exisym1  37427  regsfromsetind  37542  exlimii  37958  bj-exlimmpi  38039  bj-exlimmpbi  38040  bj-exlimmpbir  38041  dihglblem5  42621  eu2ndop1stv  48468  pgind  51216