Theorem exlimi 2218

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

Syntax hints:   → wi 4  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbalexOLD  2244  equsexv  2269  equs5av  2277  exlimih  2289  equs5aALT  2365  equs5eALT  2366  equsex  2417  exdistrf  2446  equs5a  2456  equs5e  2457  dfmoeu  2530  moanim  2614  euan  2615  moexexlem  2620  2eu6  2651  ceqsexOLD  3500  sbhypfOLD  3514  vtoclef  3532  vtoclgf  3538  vtoclg1f  3539  reusv2lem1  5356  copsexgw  5453  copsexg  5454  rexopabb  5491  ralxpf  5813  dmcoss  5941  fv3  6879  opabiota  6946  oprabidw  7421  zfregcl  9554  scottex  9845  scott0  9846  dfac5lem5  10087  zfcndpow  10576  zfcndreg  10577  zfcndinf  10578  reclem2pr  11008  mreiincl  17564  brabgaf  32543  bnj607  34913  bnj900  34926  exisym1  36419  exlimii  36826  bj-exlimmpi  36907  bj-exlimmpbi  36908  bj-exlimmpbir  36909  dihglblem5  41299  tworepnotupword  46891  eu2ndop1stv  47130  pgind  49710