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

Theorem simp1d 958
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 946 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-3an 929
This theorem is referenced by:  simp1bi  961  erinxp  6406  addcanprleml  7270  addcanprlemu  7271  ltmprr  7298  lelttrdi  8001  ixxdisj  9469  ixxss1  9470  ixxss2  9471  ixxss12  9472  iccss2  9510  iocssre  9519  icossre  9520  iccssre  9521  icodisj  9558  iccf1o  9570  fzen  9606  ioom  9821  intfracq  9876  flqdiv  9877  mulqaddmodid  9920  modsumfzodifsn  9952  addmodlteq  9954  remul  10437  sumtp  10973  crth  11643  phimullem  11644  strsetsid  11692  strleund  11747  lmfpm  12110  lmff  12116  lmtopcnp  12117  xmeter  12238  tgqioo  12337
  Copyright terms: Public domain W3C validator