Theorem exlimi 2229

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

Syntax hints:   → wi 4  ∃wex 1786  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  sbalexOLD  2255  equsexv  2280  equs5av  2288  exlimih  2300  equs5aALT  2374  equs5eALT  2375  equsex  2426  exdistrf  2455  equs5a  2465  equs5e  2466  dfmoeu  2539  moanim  2624  euan  2625  moexexlem  2630  2eu6  2660  vtoclef  3508  vtoclgf  3513  vtoclg1f  3514  reusv2lem1  5327  copsexgwOLD  5431  copsexg  5432  rexopabb  5470  ralxpf  5788  dmcossOLD  5918  fv3  6845  opabiota  6909  oprabidw  7387  zfregclOLD  9500  scottex  9800  scott0  9801  dfac5lem5  10040  zfcndpow  10530  zfcndreg  10531  zfcndinf  10532  reclem2pr  10962  mreiincl  17549  brabgaf  32698  bnj607  35098  bnj900  35111  exisym1  36652  regsfromsetind  36767  exlimii  37184  bj-exlimmpi  37265  bj-exlimmpbi  37266  bj-exlimmpbir  37267  dihglblem5  41790  eu2ndop1stv  47588  pgind  50207