Theorem exlimi 2205

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778

This theorem is referenced by:  sbalex  2230  equsexv  2254  equs5av  2265  exlimih  2278  equs5aALT  2357  equs5eALT  2358  equsex  2411  exdistrf  2440  equs5a  2450  equs5e  2451  dfmoeu  2524  moanim  2608  euan  2609  moexexlem  2614  2eu6  2645  ceqsexOLD  3513  sbhypfOLD  3529  vtoclef  3541  vtoclgf  3548  vtoclg1f  3549  rspn0OLD  4353  reusv2lem1  5398  copsexgw  5492  copsexg  5493  copsex2gOLD  5496  rexopabb  5530  0nelopabOLD  5570  ralxpf  5849  dmcoss  5974  fv3  6914  opabiota  6980  oprabidw  7450  zfregcl  9619  scottex  9910  scott0  9911  dfac5lem5  10152  zfcndpow  10641  zfcndreg  10642  zfcndinf  10643  reclem2pr  11073  mreiincl  17579  brabgaf  32477  cnvoprabOLD  32584  bnj607  34678  bnj900  34691  exisym1  36039  exlimii  36439  bj-exlimmpi  36521  bj-exlimmpbi  36522  bj-exlimmpbir  36523  dihglblem5  40901  tworepnotupword  46410  eu2ndop1stv  46643  pgind  48334