Theorem exlimi 2224

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  sbalexOLD  2250  equsexv  2275  equs5av  2283  exlimih  2295  equs5aALT  2370  equs5eALT  2371  equsex  2422  exdistrf  2451  equs5a  2461  equs5e  2462  dfmoeu  2535  moanim  2620  euan  2621  moexexlem  2626  2eu6  2657  vtoclef  3520  vtoclgf  3525  vtoclg1f  3526  reusv2lem1  5343  copsexgw  5438  copsexg  5439  rexopabb  5476  ralxpf  5795  dmcossOLD  5925  fv3  6852  opabiota  6916  oprabidw  7389  zfregclOLD  9500  scottex  9797  scott0  9798  dfac5lem5  10037  zfcndpow  10527  zfcndreg  10528  zfcndinf  10529  reclem2pr  10959  mreiincl  17515  brabgaf  32684  bnj607  35072  bnj900  35085  exisym1  36618  regsfromsetind  36669  exlimii  37032  bj-exlimmpi  37113  bj-exlimmpbi  37114  bj-exlimmpbir  37115  dihglblem5  41558  eu2ndop1stv  47371  pgind  49962