Theorem exlimi 2220

Description: Inference associated with 19.23 2214. 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 2214	. 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 2180

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

This theorem is referenced by:  sbalexOLD  2246  equsexv  2271  equs5av  2279  exlimih  2291  equs5aALT  2366  equs5eALT  2367  equsex  2418  exdistrf  2447  equs5a  2457  equs5e  2458  dfmoeu  2531  moanim  2615  euan  2616  moexexlem  2621  2eu6  2652  ceqsexOLD  3486  sbhypfOLD  3500  vtoclef  3518  vtoclgf  3524  vtoclg1f  3525  reusv2lem1  5336  copsexgw  5430  copsexg  5431  rexopabb  5468  ralxpf  5786  dmcossOLD  5915  fv3  6840  opabiota  6904  oprabidw  7377  zfregclOLD  9481  scottex  9778  scott0  9779  dfac5lem5  10018  zfcndpow  10507  zfcndreg  10508  zfcndinf  10509  reclem2pr  10939  mreiincl  17498  brabgaf  32587  bnj607  34926  bnj900  34939  exisym1  36464  exlimii  36871  bj-exlimmpi  36952  bj-exlimmpbi  36953  bj-exlimmpbir  36954  dihglblem5  41343  eu2ndop1stv  47162  pgind  49755