Theorem exlimi 2213

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

Syntax hints:   → wi 4  ∃wex 1785  Ⅎwnf 1789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-12 2174

This theorem depends on definitions:  df-bi 206  df-ex 1786  df-nf 1790

This theorem is referenced by:  sbalex  2238  equsexv  2263  equs5av  2274  exlimih  2289  equs5aALT  2365  equs5eALT  2366  equsex  2419  exdistrf  2448  equs5a  2458  equs5e  2459  dfmoeu  2537  moanim  2623  euan  2624  moexexlem  2629  2eu6  2659  ceqsex  3476  sbhypf  3489  vtoclgf  3501  vtoclg1f  3502  vtoclef  3521  rspn0OLD  4292  reusv2lem1  5324  copsexgw  5406  copsexg  5407  copsex2gOLD  5410  rexopabb  5442  0nelopabOLD  5480  ralxpf  5752  dmcoss  5877  fv3  6786  opabiota  6845  oprabidw  7299  zfregcl  9314  scottex  9627  scott0  9628  dfac5lem5  9867  zfcndpow  10356  zfcndreg  10357  zfcndinf  10358  reclem2pr  10788  mreiincl  17286  brabgaf  30927  cnvoprabOLD  31034  bnj607  32875  bnj900  32888  exisym1  34592  exlimii  34993  bj-exlimmpi  35076  bj-exlimmpbi  35077  bj-exlimmpbir  35078  dihglblem5  39291  eu2ndop1stv  44568