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

Theorem simp3d 978
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 966 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 14 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  simp3bi  981  erinxp  6457  resixp  6581  addcanprleml  7370  addcanprlemu  7371  ltmprr  7398  lelttrdi  8107  ixxdisj  9579  ixxss1  9580  ixxss2  9581  ixxss12  9582  iccsupr  9642  icodisj  9668  ioom  9931  intfracq  9986  flqdiv  9987  mulqaddmodid  10030  modsumfzodifsn  10062  cjmul  10550  sumtp  11075  crth  11745  ennnfonelemim  11782  ctiunct  11796  strsetsid  11835  strleund  11890  lmcvg  12228  lmff  12260  lmtopcnp  12261  xmeter  12425  xmetresbl  12429  tgqioo  12533  limccl  12584  limcdifap  12587  limcresi  12591  limccnpcntop  12600  limccnp2lem  12601  limccnp2cntop  12602
  Copyright terms: Public domain W3C validator