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

Theorem simp1d 1009
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 997 . 2 ((𝜓𝜒𝜃) → 𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  simp1bi  1012  erinxp  6602  addcanprleml  7591  addcanprlemu  7592  ltmprr  7619  lelttrdi  8360  ixxdisj  9877  ixxss1  9878  ixxss2  9879  ixxss12  9880  iccss2  9918  iocssre  9927  icossre  9928  iccssre  9929  icodisj  9966  iccf1o  9978  fzen  10016  ioom  10234  intfracq  10293  flqdiv  10294  mulqaddmodid  10337  modsumfzodifsn  10369  addmodlteq  10371  remul  10852  sumtp  11393  crth  12194  phimullem  12195  eulerthlem1  12197  eulerthlemfi  12198  eulerthlemrprm  12199  eulerthlema  12200  eulerthlemh  12201  eulerthlemth  12202  ctiunct  12411  strsetsid  12465  strleund  12531  mhmf  12733  submss  12744  lmfpm  13376  lmff  13382  lmtopcnp  13383  xmeter  13569  tgqioo  13680  ivthinclemlopn  13747  ivthinclemuopn  13749  limcimolemlt  13766  limcresi  13768  cosordlem  13903  relogbval  14002  relogbzcl  14003  nnlogbexp  14010
  Copyright terms: Public domain W3C validator