Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  exlimddv GIF version

Theorem exlimddv 1870
 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
StepHypRef Expression
1 exlimddv.1 . 2 (𝜑 → ∃𝑥𝜓)
2 exlimddv.2 . . . 4 ((𝜑𝜓) → 𝜒)
32ex 114 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 1791 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 13 1 (𝜑𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103  ∃wex 1468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie2 1470  ax-17 1506 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  fvmptdv2  5510  tfrlemi14d  6230  tfrexlem  6231  tfr1onlemres  6246  tfrcllemres  6259  tfrcldm  6260  erref  6449  xpdom2  6725  dom0  6732  xpen  6739  mapdom1g  6741  phplem4dom  6756  phplem4on  6761  fidceq  6763  dif1en  6773  fin0  6779  fin0or  6780  isinfinf  6791  infm  6798  en2eqpr  6801  fiuni  6866  supelti  6889  djudom  6978  difinfsn  6985  enomnilem  7010  exmidfodomrlemim  7062  exmidaclem  7069  cc2lem  7086  cc3  7088  genpml  7337  genpmu  7338  ltexprlemm  7420  ltexprlemfl  7429  ltexprlemfu  7431  suplocsr  7629  axpre-suploc  7722  eqord1  8257  nn1suc  8751  seq3f1oleml  10288  zfz1isolem1  10595  ennnfonelemim  11948  exmidunben  11950  enctlem  11956  ctiunct  11964  unct  11966  omctfn  11967  omiunct  11968  lmff  12432  txcn  12458  suplociccreex  12785  suplociccex  12786  subctctexmid  13280  exmidsbthrlem  13303  sbthom  13307
 Copyright terms: Public domain W3C validator