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

Theorem simp2d 962
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 950 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
31, 2syl 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-3an 932
This theorem is referenced by:  simp2bi  965  erinxp  6433  resixp  6557  addcanprleml  7323  addcanprlemu  7324  ltmprr  7351  lelttrdi  8055  ixxdisj  9527  ixxss1  9528  ixxss2  9529  ixxss12  9530  iccgelb  9556  iccss2  9568  icodisj  9616  ioom  9879  flqdiv  9935  mulqaddmodid  9978  modsumfzodifsn  10010  addmodlteq  10012  immul  10492  sumtp  11022  crth  11692  phimullem  11693  structn0fun  11754  strleund  11829  lmcl  12195  lmtopcnp  12200  xmeter  12364  tgqioo  12466  limcimolemlt  12513  limcresi  12515  limccnpcntop  12520
  Copyright terms: Public domain W3C validator