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  2371  equs5eALT  2372  equsex  2423  exdistrf  2452  equs5a  2462  equs5e  2463  dfmoeu  2536  moanim  2621  euan  2622  moexexlem  2627  2eu6  2658  vtoclef  3509  vtoclgf  3514  vtoclg1f  3515  reusv2lem1  5335  copsexgw  5438  copsexg  5439  rexopabb  5476  ralxpf  5795  dmcossOLD  5925  fv3  6852  opabiota  6916  oprabidw  7391  zfregclOLD  9503  scottex  9800  scott0  9801  dfac5lem5  10040  zfcndpow  10530  zfcndreg  10531  zfcndinf  10532  reclem2pr  10962  mreiincl  17549  brabgaf  32694  bnj607  35074  bnj900  35087  exisym1  36622  regsfromsetind  36737  exlimii  37154  bj-exlimmpi  37235  bj-exlimmpbi  37236  bj-exlimmpbir  37237  dihglblem5  41758  eu2ndop1stv  47585  pgind  50204