Theorem exlimi 2208

Description: Inference associated with 19.23 2202. See exlimiv 1931 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 2202	. 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 1911  ax-6 1969  ax-7 2009  ax-12 2169

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

This theorem is referenced by:  sbalex  2233  equsexv  2258  equs5av  2269  exlimih  2284  equs5aALT  2362  equs5eALT  2363  equsex  2416  exdistrf  2445  equs5a  2455  equs5e  2456  dfmoeu  2534  moanim  2620  euan  2621  moexexlem  2626  2eu6  2656  ceqsex  3483  sbhypf  3496  vtoclgf  3508  vtoclg1f  3509  vtoclef  3528  rspn0OLD  4293  reusv2lem1  5330  copsexgw  5417  copsexg  5418  copsex2gOLD  5421  rexopabb  5454  0nelopabOLD  5494  ralxpf  5768  dmcoss  5892  fv3  6822  opabiota  6883  oprabidw  7338  zfregcl  9397  scottex  9687  scott0  9688  dfac5lem5  9929  zfcndpow  10418  zfcndreg  10419  zfcndinf  10420  reclem2pr  10850  mreiincl  17350  brabgaf  30993  cnvoprabOLD  31100  bnj607  32941  bnj900  32954  exisym1  34658  exlimii  35058  bj-exlimmpi  35141  bj-exlimmpbi  35142  bj-exlimmpbir  35143  dihglblem5  39354  eu2ndop1stv  44675  tworepnotupword  46579