Theorem exlimi 2218

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

Syntax hints:   → wi 4  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbalexOLD  2244  equsexv  2269  equs5av  2277  exlimih  2289  equs5aALT  2364  equs5eALT  2365  equsex  2416  exdistrf  2445  equs5a  2455  equs5e  2456  dfmoeu  2529  moanim  2613  euan  2614  moexexlem  2619  2eu6  2650  ceqsexOLD  3488  sbhypfOLD  3502  vtoclef  3520  vtoclgf  3526  vtoclg1f  3527  reusv2lem1  5340  copsexgw  5437  copsexg  5438  rexopabb  5475  ralxpf  5793  dmcossOLD  5921  fv3  6844  opabiota  6909  oprabidw  7384  zfregclOLD  9506  scottex  9800  scott0  9801  dfac5lem5  10040  zfcndpow  10529  zfcndreg  10530  zfcndinf  10531  reclem2pr  10961  mreiincl  17516  brabgaf  32569  bnj607  34885  bnj900  34898  exisym1  36400  exlimii  36807  bj-exlimmpi  36888  bj-exlimmpbi  36889  bj-exlimmpbir  36890  dihglblem5  41280  tworepnotupword  46871  eu2ndop1stv  47113  pgind  49706