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

Theorem simp2d 979
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 967 . 2 ((𝜓𝜒𝜃) → 𝜒)
31, 2syl 14 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947
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 949
This theorem is referenced by:  simp2bi  982  erinxp  6471  resixp  6595  addcanprleml  7390  addcanprlemu  7391  ltmprr  7418  lelttrdi  8156  ixxdisj  9654  ixxss1  9655  ixxss2  9656  ixxss12  9657  iccgelb  9683  iccss2  9695  icodisj  9743  ioom  10006  flqdiv  10062  mulqaddmodid  10105  modsumfzodifsn  10137  addmodlteq  10139  immul  10619  sumtp  11151  crth  11827  phimullem  11828  ctiunct  11880  structn0fun  11899  strleund  11974  lmcl  12341  lmtopcnp  12346  xmeter  12532  tgqioo  12643  ivthinclemlopn  12710  ivthinclemuopn  12712  limcimolemlt  12729  limcresi  12731  limccnpcntop  12740  limccnp2lem  12741  limccnp2cntop  12742  cosordlem  12857
  Copyright terms: Public domain W3C validator