Theorem exlimi 2220

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

Syntax hints:   → wi 4  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  sbalexOLD  2246  equsexv  2271  equs5av  2279  exlimih  2291  equs5aALT  2366  equs5eALT  2367  equsex  2418  exdistrf  2447  equs5a  2457  equs5e  2458  dfmoeu  2531  moanim  2615  euan  2616  moexexlem  2621  2eu6  2652  vtoclef  3516  vtoclgf  3521  vtoclg1f  3522  reusv2lem1  5338  copsexgw  5433  copsexg  5434  rexopabb  5471  ralxpf  5791  dmcossOLD  5920  fv3  6846  opabiota  6910  oprabidw  7383  zfregclOLD  9487  scottex  9784  scott0  9785  dfac5lem5  10024  zfcndpow  10513  zfcndreg  10514  zfcndinf  10515  reclem2pr  10945  mreiincl  17504  brabgaf  32596  bnj607  34935  bnj900  34948  exisym1  36475  exlimii  36882  bj-exlimmpi  36963  bj-exlimmpbi  36964  bj-exlimmpbir  36965  dihglblem5  41403  eu2ndop1stv  47230  pgind  49823