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

Theorem simp3d 996
 Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1
Assertion
Ref Expression
simp3d

Proof of Theorem simp3d
StepHypRef Expression
1 3simp1d.1 . 2
2 simp3 984 . 2
31, 2syl 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   w3a 963 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 965 This theorem is referenced by:  simp3bi  999  erinxp  6512  resixp  6636  addcanprleml  7466  addcanprlemu  7467  ltmprr  7494  lelttrdi  8232  ixxdisj  9736  ixxss1  9737  ixxss2  9738  ixxss12  9739  iccsupr  9799  icodisj  9825  ioom  10089  intfracq  10144  flqdiv  10145  mulqaddmodid  10188  modsumfzodifsn  10220  cjmul  10709  sumtp  11235  crth  11956  ennnfonelemim  11993  ctiunct  12009  strsetsid  12051  strleund  12106  lmcvg  12445  lmff  12477  lmtopcnp  12478  xmeter  12664  xmetresbl  12668  tgqioo  12775  ivthinclemlopn  12842  ivthinclemuopn  12844  limccl  12856  limcdifap  12859  limcresi  12863  limccnpcntop  12872  limccnp2lem  12873  limccnp2cntop  12874  limccoap  12875  cosordlem  12998  relogbval  13096  relogbzcl  13097  nnlogbexp  13104
 Copyright terms: Public domain W3C validator