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

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

Proof of Theorem simp1d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp1 915 . 2 ((𝜓𝜒𝜃) → 𝜓)
31, 2syl 14 1 (𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 896 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103 This theorem depends on definitions:  df-bi 114  df-3an 898 This theorem is referenced by:  simp1bi  930  erinxp  6211  addcanprleml  6770  addcanprlemu  6771  ltmprr  6798  lelttrdi  7495  ixxdisj  8873  ixxss1  8874  ixxss2  8875  ixxss12  8876  iccss2  8914  iocssre  8923  icossre  8924  iccssre  8925  icodisj  8961  iccf1o  8973  fzen  9009  ioom  9217  intfracq  9270  flqdiv  9271  mulqaddmodid  9314  modsumfzodifsn  9346  addmodlteq  9348  remul  9700
 Copyright terms: Public domain W3C validator