Theorem exlimi 2225

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

Syntax hints:   → wi 4  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  sbalexOLD  2251  equsexv  2276  equs5av  2284  exlimih  2296  equs5aALT  2370  equs5eALT  2371  equsex  2422  exdistrf  2451  equs5a  2461  equs5e  2462  dfmoeu  2535  moanim  2620  euan  2621  moexexlem  2626  2eu6  2657  vtoclef  3508  vtoclgf  3513  vtoclg1f  3514  reusv2lem1  5340  copsexgwOLD  5444  copsexg  5445  rexopabb  5483  ralxpf  5801  dmcossOLD  5931  fv3  6858  opabiota  6922  oprabidw  7398  zfregclOLD  9510  scottex  9809  scott0  9810  dfac5lem5  10049  zfcndpow  10539  zfcndreg  10540  zfcndinf  10541  reclem2pr  10971  mreiincl  17558  brabgaf  32679  bnj607  35058  bnj900  35071  exisym1  36606  regsfromsetind  36721  exlimii  37138  bj-exlimmpi  37219  bj-exlimmpbi  37220  bj-exlimmpbir  37221  dihglblem5  41744  eu2ndop1stv  47573  pgind  50192