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

Theorem simp1d 993
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 981 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 962
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 964
This theorem is referenced by:  simp1bi  996  erinxp  6503  addcanprleml  7434  addcanprlemu  7435  ltmprr  7462  lelttrdi  8200  ixxdisj  9698  ixxss1  9699  ixxss2  9700  ixxss12  9701  iccss2  9739  iocssre  9748  icossre  9749  iccssre  9750  icodisj  9787  iccf1o  9799  fzen  9835  ioom  10050  intfracq  10105  flqdiv  10106  mulqaddmodid  10149  modsumfzodifsn  10181  addmodlteq  10183  remul  10656  sumtp  11195  crth  11911  phimullem  11912  ctiunct  11964  strsetsid  12006  strleund  12061  lmfpm  12426  lmff  12432  lmtopcnp  12433  xmeter  12619  tgqioo  12730  ivthinclemlopn  12797  ivthinclemuopn  12799  limcimolemlt  12816  limcresi  12818  cosordlem  12952
  Copyright terms: Public domain W3C validator