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

Theorem simp2d 995
 Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1 (𝜑 → (𝜓𝜒𝜃))
Assertion
Ref Expression
simp2d (𝜑𝜒)

Proof of Theorem simp2d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp2 983 . 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 This theorem depends on definitions:  df-bi 116  df-3an 965 This theorem is referenced by:  simp2bi  998  erinxp  6511  resixp  6635  addcanprleml  7446  addcanprlemu  7447  ltmprr  7474  lelttrdi  8212  ixxdisj  9716  ixxss1  9717  ixxss2  9718  ixxss12  9719  iccgelb  9745  iccss2  9757  icodisj  9805  ioom  10069  flqdiv  10125  mulqaddmodid  10168  modsumfzodifsn  10200  addmodlteq  10202  immul  10683  sumtp  11215  crth  11936  phimullem  11937  ctiunct  11989  structn0fun  12011  strleund  12086  lmcl  12453  lmtopcnp  12458  xmeter  12644  tgqioo  12755  ivthinclemlopn  12822  ivthinclemuopn  12824  limcimolemlt  12841  limcresi  12843  limccnpcntop  12852  limccnp2lem  12853  limccnp2cntop  12854  cosordlem  12978
 Copyright terms: Public domain W3C validator