Theorem exlimi 2213

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

Syntax hints:   → wi 4  ∃wex 1776  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173

This theorem depends on definitions:  df-bi 209  df-ex 1777  df-nf 1781

This theorem is referenced by:  equs5av  2275  exlimih  2293  equs5aALT  2380  equs5eALT  2381  equsex  2436  exdistrf  2465  equs5a  2476  equs5e  2477  dfmoeu  2614  moanim  2701  euan  2702  moexexlem  2707  2eu6  2740  ceqsex  3540  sbhypf  3552  vtoclgf  3565  vtoclg1f  3566  vtoclef  3582  rspn0  4312  reusv2lem1  5290  copsexgw  5373  copsexg  5374  copsex2g  5376  rexopabb  5407  0nelopab  5444  ralxpf  5711  dmcoss  5836  fv3  6682  opabiota  6740  oprabidw  7181  zfregcl  9052  scottex  9308  scott0  9309  dfac5lem5  9547  zfcndpow  10032  zfcndreg  10033  zfcndinf  10034  reclem2pr  10464  mreiincl  16861  brabgaf  30353  cnvoprabOLD  30450  bnj607  32183  bnj900  32196  exisym1  33767  exlimii  34149  bj-exlimmpi  34223  bj-exlimmpbi  34224  bj-exlimmpbir  34225  dihglblem5  38428  eu2ndop1stv  43318