Theorem exlimi 2259

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

Syntax hints:   → wi 4  ∃wex 1806  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  sbalexOLD  2285  equsexv  2310  equs5av  2318  exlimih  2330  equs5aALT  2404  equs5eALT  2405  equsex  2456  exdistrf  2485  equs5a  2495  equs5e  2496  dfmoeu  2569  moanim  2654  euan  2655  moexexlem  2660  2eu6  2690  vtoclef  3538  vtoclgf  3543  vtoclg1f  3544  reusv2lem1  5367  copsexgwOLD  5471  copsexg  5472  rexopabb  5510  ralxpf  5830  dmcossOLD  5964  fv3  6897  opabiota  6961  oprabidw  7439  zfregclOLD  9553  scottex  9855  scott0  9856  dfac5lem5  10107  zfcndpow  10597  zfcndreg  10598  zfcndinf  10599  reclem2pr  11029  mreiincl  17644  brabgaf  32888  bnj607  35245  bnj900  35258  exisym1  36820  regsfromsetind  36935  exlimii  37351  bj-exlimmpi  37432  bj-exlimmpbi  37433  bj-exlimmpbir  37434  dihglblem5  41957  eu2ndop1stv  47744  pgind  50373