Theorem exlimddv 1898

Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
exlimddv.1	⊢ (𝜑 → ∃𝑥𝜓)
exlimddv.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
exlimddv	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimddv

Step	Hyp	Ref	Expression
1		exlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥𝜓)
2		exlimddv.2	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 115	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	exlimdv 1819	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  fvmptdv2  5607  tfrlemi14d  6336  tfrexlem  6337  tfr1onlemres  6352  tfrcllemres  6365  tfrcldm  6366  erref  6557  xpdom2  6833  dom0  6840  xpen  6847  mapdom1g  6849  phplem4dom  6864  phplem4on  6869  fidceq  6871  dif1en  6881  fin0  6887  fin0or  6888  isinfinf  6899  infm  6906  en2eqpr  6909  fiuni  6979  supelti  7003  djudom  7094  difinfsn  7101  enomnilem  7138  enmkvlem  7161  enwomnilem  7169  exmidfodomrlemim  7202  exmidaclem  7209  cc2lem  7267  cc3  7269  genpml  7518  genpmu  7519  ltexprlemm  7601  ltexprlemfl  7610  ltexprlemfu  7612  suplocsr  7810  axpre-suploc  7903  eqord1  8442  nn1suc  8940  seq3f1oleml  10505  zfz1isolem1  10822  nninfdcex  11956  zsupssdc  11957  eulerth  12235  ennnfonelemim  12427  exmidunben  12429  enctlem  12435  ctiunct  12443  unct  12445  omctfn  12446  omiunct  12447  issubg2m  13054  lmff  13834  txcn  13860  suplociccreex  14187  suplociccex  14188  subctctexmid  14835  exmidsbthrlem  14855  sbthom  14859