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

Theorem simp2d 928
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Assertion
Ref Expression
simp2d  |-  ( ph  ->  ch )

Proof of Theorem simp2d
StepHypRef Expression
1 3simp1d.1 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
2 simp2 916 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
31, 2syl 14 1  |-  ( ph  ->  ch )
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  ax-ia2 104
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simp2bi  931  erinxp  6211  addcanprleml  6770  addcanprlemu  6771  ltmprr  6798  lelttrdi  7495  ixxdisj  8873  ixxss1  8874  ixxss2  8875  ixxss12  8876  iccgelb  8902  iccss2  8914  icodisj  8961  ioom  9217  flqdiv  9271  mulqaddmodid  9314  modsumfzodifsn  9346  addmodlteq  9348  immul  9707
  Copyright terms: Public domain W3C validator