Theorem exlimi 2222

Description: Inference associated with 19.23 2216. 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 2216	. 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 2182

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

This theorem is referenced by:  sbalexOLD  2248  equsexv  2273  equs5av  2281  exlimih  2293  equs5aALT  2368  equs5eALT  2369  equsex  2420  exdistrf  2449  equs5a  2459  equs5e  2460  dfmoeu  2533  moanim  2617  euan  2618  moexexlem  2623  2eu6  2654  vtoclef  3517  vtoclgf  3522  vtoclg1f  3523  reusv2lem1  5340  copsexgw  5435  copsexg  5436  rexopabb  5473  ralxpf  5792  dmcossOLD  5922  fv3  6849  opabiota  6913  oprabidw  7386  zfregclOLD  9492  scottex  9789  scott0  9790  dfac5lem5  10029  zfcndpow  10518  zfcndreg  10519  zfcndinf  10520  reclem2pr  10950  mreiincl  17506  brabgaf  32610  bnj607  35000  bnj900  35013  exisym1  36540  exlimii  36948  bj-exlimmpi  37029  bj-exlimmpbi  37030  bj-exlimmpbir  37031  dihglblem5  41470  eu2ndop1stv  47287  pgind  49878