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  5798  tfrlemi14d  6608  tfrexlem  6609  tfr1onlemres  6624  tfrcllemres  6637  tfrcldm  6638  erref  6831  1dom1el  7112  en2  7117  en2m  7118  xpdom2  7134  dom0  7143  xpen  7150  mapdom1g  7152  phplem4dom  7168  phplem4on  7174  fidceq  7176  dif1en  7188  fin0  7194  fin0or  7195  isinfinf  7206  eqsndc  7215  infm  7216  en2eqpr  7219  fiuni  7318  supelti  7349  djudom  7440  difinfsn  7447  enomnilem  7485  enmkvlem  7508  enwomnilem  7516  exmidfodomrlemim  7560  exmidaclem  7571  cc2lem  7639  cc3  7641  genpml  7891  genpmu  7892  ltexprlemm  7974  ltexprlemfl  7983  ltexprlemfu  7985  suplocsr  8183  axpre-suploc  8276  eqord1  8819  nn1suc  9333  nninfdcex  10690  zsupssdc  10691  seq3f1oleml  10975  zfz1isolem1  11315  eulerth  13041  4sqlem14  13213  4sqlem17  13216  4sqlem18  13217  ennnfonelemim  13374  exmidunben  13376  enctlem  13382  ctiunct  13390  unct  13392  omctfn  13393  omiunct  13394  relelbasov  13475  issubg2m  14052  gsump1  14248  gsumf1ofi  14251  gsummhmfi  14265  gsumressfi  14268  opprringb  14496  lmff  15487  txcn  15513  suplociccreex  15862  suplociccex  15863  wlkvtxiedg  16803  wlkvtxiedgg  16804  wlkreslem  16836  eulerpathum  16939  3dom  17235  subctctexmid  17247  exmidsbthrlem  17285  sbthom  17289