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

Theorem simp3d 953
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
simp3d  |-  ( ph  ->  th )

Proof of Theorem simp3d
StepHypRef Expression
1 3simp1d.1 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
2 simp3 941 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 14 1  |-  ( ph  ->  th )
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  6239  addcanprleml  6855  addcanprlemu  6856  ltmprr  6883  lelttrdi  7586  ixxdisj  8991  ixxss1  8992  ixxss2  8993  ixxss12  8994  iccsupr  9054  icodisj  9079  ioom  9336  intfracq  9391  flqdiv  9392  mulqaddmodid  9435  modsumfzodifsn  9467  cjmul  9899
  Copyright terms: Public domain W3C validator