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

Theorem simp2d 952
 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 940 . 2 ((𝜓𝜒𝜃) → 𝜒)
31, 2syl 14 1 (𝜑𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 920 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105 This theorem depends on definitions:  df-bi 115  df-3an 922 This theorem is referenced by:  simp2bi  955  erinxp  6246  addcanprleml  6866  addcanprlemu  6867  ltmprr  6894  lelttrdi  7597  ixxdisj  9002  ixxss1  9003  ixxss2  9004  ixxss12  9005  iccgelb  9031  iccss2  9043  icodisj  9090  ioom  9347  flqdiv  9403  mulqaddmodid  9446  modsumfzodifsn  9478  addmodlteq  9480  immul  9904
 Copyright terms: Public domain W3C validator