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

Theorem simp1d 916
 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 904 . 2 ((𝜓𝜒𝜃) → 𝜓)
31, 2syl 14 1 (𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  simp1bi  919  erinxp  6180  addcanprleml  6712  addcanprlemu  6713  ltmprr  6740  lelttrdi  7421  ixxdisj  8772  ixxss1  8773  ixxss2  8774  ixxss12  8775  iccss2  8813  iocssre  8822  icossre  8823  iccssre  8824  icodisj  8860  iccf1o  8872  fzen  8907  intfracq  9162  flqdiv  9163  remul  9472
 Copyright terms: Public domain W3C validator