Theorem exlimi 2182

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

Syntax hints:   → wi 4  ∃wex 1761  Ⅎwnf 1765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-12 2141

This theorem depends on definitions:  df-bi 208  df-ex 1762  df-nf 1766

This theorem is referenced by:  exlimih  2263  equs5aALT  2341  equs5eALT  2342  equsex  2396  exdistrf  2426  equs5a  2437  equs5e  2438  dfmoeu  2572  moanim  2673  euan  2674  moexexlem  2681  2eu6  2714  ceqsex  3483  sbhypf  3495  vtoclgf  3508  vtoclg1f  3509  vtoclef  3526  rspn0  4233  reusv2lem1  5190  copsexg  5273  copsex2g  5275  rexopabb  5305  0nelopab  5340  ralxpf  5603  dmcoss  5723  fv3  6556  opabiota  6613  zfregcl  8904  scottex  9160  scott0  9161  dfac5lem5  9399  zfcndpow  9884  zfcndreg  9885  zfcndinf  9886  reclem2pr  10316  mreiincl  16696  brabgaf  30049  cnvoprabOLD  30144  bnj607  31804  bnj900  31817  exisym1  33381  exlimii  33724  bj-exlimmpi  33799  bj-exlimmpbi  33800  bj-exlimmpbir  33801  dihglblem5  37965  eu2ndop1stv  42840