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  2277  exlimih  2289  equs5aALT  2364  equs5eALT  2365  equsex  2416  exdistrf  2445  equs5a  2455  equs5e  2456  dfmoeu  2529  moanim  2613  euan  2614  moexexlem  2619  2eu6  2650  ceqsexOLD  3497  sbhypfOLD  3511  vtoclef  3529  vtoclgf  3535  vtoclg1f  3536  reusv2lem1  5353  copsexgw  5450  copsexg  5451  rexopabb  5488  ralxpf  5810  dmcoss  5938  fv3  6876  opabiota  6943  oprabidw  7418  zfregcl  9547  scottex  9838  scott0  9839  dfac5lem5  10080  zfcndpow  10569  zfcndreg  10570  zfcndinf  10571  reclem2pr  11001  mreiincl  17557  brabgaf  32536  bnj607  34906  bnj900  34919  exisym1  36412  exlimii  36819  bj-exlimmpi  36900  bj-exlimmpbi  36901  bj-exlimmpbir  36902  dihglblem5  41292  tworepnotupword  46884  eu2ndop1stv  47126  pgind  49706