Theorem exlimddv 1954

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 1872	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 13	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  fvmptdv2  5795  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemres  6620  tfrcllemres  6633  tfrcldm  6634  erref  6827  1dom1el  7107  en2  7112  en2m  7113  xpdom2  7129  dom0  7138  xpen  7145  mapdom1g  7147  phplem4dom  7163  phplem4on  7169  fidceq  7171  dif1en  7183  fin0  7189  fin0or  7190  isinfinf  7201  eqsndc  7210  infm  7211  en2eqpr  7214  fiuni  7312  supelti  7343  djudom  7434  difinfsn  7441  enomnilem  7479  enmkvlem  7502  enwomnilem  7510  exmidfodomrlemim  7554  exmidaclem  7565  cc2lem  7633  cc3  7635  genpml  7885  genpmu  7886  ltexprlemm  7968  ltexprlemfl  7977  ltexprlemfu  7979  suplocsr  8177  axpre-suploc  8270  eqord1  8813  nn1suc  9326  nninfdcex  10683  zsupssdc  10684  seq3f1oleml  10967  zfz1isolem1  11307  eulerth  13033  4sqlem14  13205  4sqlem17  13208  4sqlem18  13209  ennnfonelemim  13366  exmidunben  13368  enctlem  13374  ctiunct  13382  unct  13384  omctfn  13385  omiunct  13386  relelbasov  13467  issubg2m  14043  gsump1  14208  gsumf1ofi  14211  gsummhmfi  14215  gsumressfi  14218  opprringb  14437  lmff  15402  txcn  15428  suplociccreex  15777  suplociccex  15778  wlkvtxiedg  16708  wlkvtxiedgg  16709  wlkreslem  16741  eulerpathum  16844  3dom  17140  subctctexmid  17152  exmidsbthrlem  17189  sbthom  17193