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

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

Proof of Theorem simp3d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp3 941 . 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  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simp3bi  956  erinxp  6296  addcanprleml  7076  addcanprlemu  7077  ltmprr  7104  lelttrdi  7807  ixxdisj  9216  ixxss1  9217  ixxss2  9218  ixxss12  9219  iccsupr  9279  icodisj  9304  ioom  9561  intfracq  9616  flqdiv  9617  mulqaddmodid  9660  modsumfzodifsn  9692  cjmul  10146  crth  10980
  Copyright terms: Public domain W3C validator