Theorem exlimi 2217

Description: Inference associated with 19.23 2211. 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 2211	. 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 2007  ax-12 2177

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

This theorem is referenced by:  sbalexOLD  2243  equsexv  2268  equs5av  2277  exlimih  2289  equs5aALT  2369  equs5eALT  2370  equsex  2423  exdistrf  2452  equs5a  2462  equs5e  2463  dfmoeu  2536  moanim  2620  euan  2621  moexexlem  2626  2eu6  2657  ceqsexOLD  3531  sbhypfOLD  3545  vtoclef  3563  vtoclgf  3569  vtoclg1f  3570  reusv2lem1  5398  copsexgw  5495  copsexg  5496  rexopabb  5533  ralxpf  5857  dmcoss  5985  fv3  6924  opabiota  6991  oprabidw  7462  zfregcl  9634  scottex  9925  scott0  9926  dfac5lem5  10167  zfcndpow  10656  zfcndreg  10657  zfcndinf  10658  reclem2pr  11088  mreiincl  17639  brabgaf  32620  bnj607  34930  bnj900  34943  exisym1  36425  exlimii  36832  bj-exlimmpi  36913  bj-exlimmpbi  36914  bj-exlimmpbir  36915  dihglblem5  41300  tworepnotupword  46901  eu2ndop1stv  47137  pgind  49236