Theorem exlimi 2253

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

Syntax hints:   → wi 4  ∃wex 1809  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced by:  sbalexOLD  2279  equsexv  2304  equs5av  2312  exlimih  2324  equs5aALT  2398  equs5eALT  2399  equsex  2450  exdistrf  2479  equs5a  2489  equs5e  2490  dfmoeu  2563  moanim  2648  euan  2649  moexexlem  2654  2eu6  2684  vtoclef  3530  vtoclgf  3535  vtoclg1f  3536  reusv2lem1  5371  copsexgwOLD  5475  copsexg  5476  rexopabb  5514  ralxpf  5834  dmcossOLD  5968  fv3  6901  opabiota  6965  oprabidw  7443  zfregclOLD  9558  scottex  9860  scott0  9861  dfac5lem5  10112  zfcndpow  10602  zfcndreg  10603  zfcndinf  10604  reclem2pr  11034  mreiincl  17649  brabgaf  32932  bnj607  35285  bnj900  35298  exisym1  36916  regsfromsetind  37031  exlimii  37447  bj-exlimmpi  37528  bj-exlimmpbi  37529  bj-exlimmpbir  37530  dihglblem5  42053  eu2ndop1stv  47845  pgind  50478