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  3522  vtoclgf  3527  vtoclg1f  3528  reusv2lem1  5345  copsexgw  5446  copsexg  5447  rexopabb  5484  ralxpf  5803  dmcossOLD  5933  fv3  6860  opabiota  6924  oprabidw  7399  zfregclOLD  9512  scottex  9809  scott0  9810  dfac5lem5  10049  zfcndpow  10539  zfcndreg  10540  zfcndinf  10541  reclem2pr  10971  mreiincl  17527  brabgaf  32695  bnj607  35091  bnj900  35104  exisym1  36637  regsfromsetind  36688  exlimii  37076  bj-exlimmpi  37157  bj-exlimmpbi  37158  bj-exlimmpbir  37159  dihglblem5  41671  eu2ndop1stv  47482  pgind  50073