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

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

Proof of Theorem simp1d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp1 982 . 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 This theorem depends on definitions:  df-bi 116  df-3an 965 This theorem is referenced by:  simp1bi  997  erinxp  6543  addcanprleml  7513  addcanprlemu  7514  ltmprr  7541  lelttrdi  8280  ixxdisj  9785  ixxss1  9786  ixxss2  9787  ixxss12  9788  iccss2  9826  iocssre  9835  icossre  9836  iccssre  9837  icodisj  9874  iccf1o  9886  fzen  9923  ioom  10138  intfracq  10197  flqdiv  10198  mulqaddmodid  10241  modsumfzodifsn  10273  addmodlteq  10275  remul  10749  sumtp  11288  crth  12068  phimullem  12069  eulerthlem1  12071  eulerthlemfi  12072  eulerthlemrprm  12073  eulerthlema  12074  eulerthlemh  12075  eulerthlemth  12076  ctiunct  12128  strsetsid  12170  strleund  12225  lmfpm  12590  lmff  12596  lmtopcnp  12597  xmeter  12783  tgqioo  12894  ivthinclemlopn  12961  ivthinclemuopn  12963  limcimolemlt  12980  limcresi  12982  cosordlem  13117  relogbval  13215  relogbzcl  13216  nnlogbexp  13223
 Copyright terms: Public domain W3C validator