Theorem exlimi 2252

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1808  Ⅎwnf 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1809  df-nf 1813

This theorem is used by:  sbalexOLD  2278  equsexv  2303  equs5av  2311  exlimih  2323  equs5aALT  2397  equs5eALT  2398  equsex  2449  exdistrf  2478  equs5a  2488  equs5e  2489  dfmoeu  2562  moanim  2647  euan  2648  moexexlem  2653  2eu6  2683  vtoclef  3528  vtoclgf  3533  vtoclg1f  3534  reusv2lem1  5368  copsexgwOLD  5472  copsexg  5473  rexopabb  5511  ralxpf  5831  dmcossOLD  5965  fv3  6899  opabiota  6963  oprabidw  7443  zfregclOLD  9555  scottexOLD  9861  scott0b  9864  scott0OLD  9865  dfac5lem5  10118  zfcndpow  10607  zfcndreg  10608  zfcndinf  10609  reclem2pr  11039  mreiincl  17654  brabgaf  32962  bnj607  35313  bnj900  35326  exisym1  36963  regsfromsetind  37078  exlimii  37494  bj-exlimmpi  37575  bj-exlimmpbi  37576  bj-exlimmpbir  37577  dihglblem5  42100  eu2ndop1stv  47890  pgind  50523