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

Theorem simp2d 926
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1 (𝜑 → (𝜓𝜒𝜃))
Assertion
Ref Expression
simp2d (𝜑𝜒)

Proof of Theorem simp2d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp2 914 . 2 ((𝜓𝜒𝜃) → 𝜒)
31, 2syl 14 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114  df-3an 896
This theorem is referenced by:  simp2bi  929  erinxp  6208  addcanprleml  6740  addcanprlemu  6741  ltmprr  6768  lelttrdi  7465  ixxdisj  8843  ixxss1  8844  ixxss2  8845  ixxss12  8846  iccgelb  8872  iccss2  8884  icodisj  8931  flqdiv  9236  mulqaddmodid  9279  modsumfzodifsn  9311  addmodlteq  9313  immul  9671
  Copyright terms: Public domain W3C validator