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

Theorem simp1d 951
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
simp1d  |-  ( ph  ->  ps )

Proof of Theorem simp1d
StepHypRef Expression
1 3simp1d.1 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
2 simp1 939 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 14 1  |-  ( ph  ->  ps )
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
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simp1bi  954  erinxp  6295  addcanprleml  7075  addcanprlemu  7076  ltmprr  7103  lelttrdi  7806  ixxdisj  9215  ixxss1  9216  ixxss2  9217  ixxss12  9218  iccss2  9256  iocssre  9265  icossre  9266  iccssre  9267  icodisj  9303  iccf1o  9315  fzen  9351  ioom  9560  intfracq  9615  flqdiv  9616  mulqaddmodid  9659  modsumfzodifsn  9691  addmodlteq  9693  remul  10132  crth  10979  phimullem  10980
  Copyright terms: Public domain W3C validator