Theorem exlimi 2218

Description: Inference associated with 19.23 2212. See exlimiv 1929 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 1796	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1777  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  sbalexOLD  2244  equsexv  2269  equs5av  2280  exlimih  2293  equs5aALT  2372  equs5eALT  2373  equsex  2426  exdistrf  2455  equs5a  2465  equs5e  2466  dfmoeu  2539  moanim  2623  euan  2624  moexexlem  2629  2eu6  2660  ceqsexOLD  3541  sbhypfOLD  3557  vtoclef  3575  vtoclgf  3581  vtoclg1f  3582  reusv2lem1  5416  copsexgw  5510  copsexg  5511  rexopabb  5547  0nelopabOLD  5587  ralxpf  5871  dmcoss  5997  fv3  6938  opabiota  7004  oprabidw  7479  zfregcl  9663  scottex  9954  scott0  9955  dfac5lem5  10196  zfcndpow  10685  zfcndreg  10686  zfcndinf  10687  reclem2pr  11117  mreiincl  17654  brabgaf  32630  cnvoprabOLD  32734  bnj607  34892  bnj900  34905  exisym1  36390  exlimii  36797  bj-exlimmpi  36878  bj-exlimmpbi  36879  bj-exlimmpbir  36880  dihglblem5  41255  tworepnotupword  46805  eu2ndop1stv  47040  pgind  48809