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

Theorem simp1d 1004
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 992 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-3an 975
This theorem is referenced by:  simp1bi  1007  erinxp  6583  addcanprleml  7563  addcanprlemu  7564  ltmprr  7591  lelttrdi  8332  ixxdisj  9847  ixxss1  9848  ixxss2  9849  ixxss12  9850  iccss2  9888  iocssre  9897  icossre  9898  iccssre  9899  icodisj  9936  iccf1o  9948  fzen  9986  ioom  10204  intfracq  10263  flqdiv  10264  mulqaddmodid  10307  modsumfzodifsn  10339  addmodlteq  10341  remul  10823  sumtp  11364  crth  12165  phimullem  12166  eulerthlem1  12168  eulerthlemfi  12169  eulerthlemrprm  12170  eulerthlema  12171  eulerthlemh  12172  eulerthlemth  12173  ctiunct  12382  strsetsid  12436  strleund  12493  mhmf  12675  submss  12685  lmfpm  12996  lmff  13002  lmtopcnp  13003  xmeter  13189  tgqioo  13300  ivthinclemlopn  13367  ivthinclemuopn  13369  limcimolemlt  13386  limcresi  13388  cosordlem  13523  relogbval  13622  relogbzcl  13623  nnlogbexp  13630
  Copyright terms: Public domain W3C validator