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

Theorem simp1d 1011
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 999 . 2 ((𝜓𝜒𝜃) → 𝜓)
31, 2syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 980
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 982
This theorem is referenced by:  simp1bi  1014  erinxp  6636  exmidapne  7290  addcanprleml  7644  addcanprlemu  7645  ltmprr  7672  lelttrdi  8414  ixxdisj  9935  ixxss1  9936  ixxss2  9937  ixxss12  9938  iccss2  9976  iocssre  9985  icossre  9986  iccssre  9987  icodisj  10024  iccf1o  10036  fzen  10075  ioom  10293  intfracq  10353  flqdiv  10354  mulqaddmodid  10397  modsumfzodifsn  10429  addmodlteq  10431  remul  10916  sumtp  11457  crth  12259  phimullem  12260  eulerthlem1  12262  eulerthlemfi  12263  eulerthlemrprm  12264  eulerthlema  12265  eulerthlemh  12266  eulerthlemth  12267  ctiunct  12494  strsetsid  12548  strleund  12618  strext  12620  mhmf  12932  submss  12943  eqger  13180  eqgcpbl  13184  lmodvscl  13638  lssssg  13693  rnglidlmsgrp  13830  2idlcpblrng  13855  lmfpm  14220  lmff  14226  lmtopcnp  14227  xmeter  14413  tgqioo  14524  ivthinclemlopn  14591  ivthinclemuopn  14593  limcimolemlt  14610  limcresi  14612  cosordlem  14747  relogbval  14846  relogbzcl  14847  nnlogbexp  14854
  Copyright terms: Public domain W3C validator