Theorem exlimi 2218

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

Syntax hints:   → wi 4  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbalexOLD  2244  equsexv  2269  equs5av  2278  exlimih  2290  equs5aALT  2369  equs5eALT  2370  equsex  2423  exdistrf  2452  equs5a  2462  equs5e  2463  dfmoeu  2536  moanim  2620  euan  2621  moexexlem  2626  2eu6  2657  ceqsexOLD  3515  sbhypfOLD  3529  vtoclef  3547  vtoclgf  3553  vtoclg1f  3554  reusv2lem1  5373  copsexgw  5470  copsexg  5471  rexopabb  5508  ralxpf  5831  dmcoss  5959  fv3  6899  opabiota  6966  oprabidw  7441  zfregcl  9613  scottex  9904  scott0  9905  dfac5lem5  10146  zfcndpow  10635  zfcndreg  10636  zfcndinf  10637  reclem2pr  11067  mreiincl  17613  brabgaf  32593  bnj607  34952  bnj900  34965  exisym1  36447  exlimii  36854  bj-exlimmpi  36935  bj-exlimmpbi  36936  bj-exlimmpbir  36937  dihglblem5  41322  tworepnotupword  46882  eu2ndop1stv  47121  pgind  49548