Theorem exlimi 2217

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

Syntax hints:   → wi 4  ∃wex 1787  Ⅎwnf 1791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-12 2177

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792

This theorem is referenced by:  sbalex  2242  equs5av  2277  exlimih  2292  equs5aALT  2365  equs5eALT  2366  equsex  2417  exdistrf  2446  equs5a  2456  equs5e  2457  dfmoeu  2535  moanim  2621  euan  2622  moexexlem  2627  2eu6  2657  ceqsex  3444  sbhypf  3457  vtoclgf  3469  vtoclg1f  3470  vtoclef  3489  rspn0OLD  4254  reusv2lem1  5276  copsexgw  5358  copsexg  5359  copsex2gOLD  5362  rexopabb  5394  0nelopabOLD  5432  ralxpf  5700  dmcoss  5825  fv3  6713  opabiota  6772  oprabidw  7222  zfregcl  9188  scottex  9466  scott0  9467  dfac5lem5  9706  zfcndpow  10195  zfcndreg  10196  zfcndinf  10197  reclem2pr  10627  mreiincl  17053  brabgaf  30621  cnvoprabOLD  30729  bnj607  32563  bnj900  32576  exisym1  34299  exlimii  34700  bj-exlimmpi  34784  bj-exlimmpbi  34785  bj-exlimmpbir  34786  dihglblem5  38998  eu2ndop1stv  44232