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

Theorem sylnib 666
 Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnib.1 (𝜑 → ¬ 𝜓)
sylnib.2 (𝜓𝜒)
Assertion
Ref Expression
sylnib (𝜑 → ¬ 𝜒)

Proof of Theorem sylnib
StepHypRef Expression
1 sylnib.1 . 2 (𝜑 → ¬ 𝜓)
2 sylnib.2 . . 3 (𝜓𝜒)
32a1i 9 . 2 (𝜑 → (𝜓𝜒))
41, 3mtbid 662 1 (𝜑 → ¬ 𝜒)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  sylnibr  667  neqcomd  2146  inssdif0im  3437  undifexmid  4127  ordtriexmidlem2  4447  dmsn0el  5020  fidifsnen  6776  ctssdccl  7013  onntri35  7117  onntri45  7120  ltpopr  7456  caucvgprprlemnbj  7554  xrlttri3  9642  fzneuz  9941  iseqf1olemqcl  10319  iseqf1olemnab  10321  iseqf1olemab  10322  exp3val  10355  pwle2  13410
 Copyright terms: Public domain W3C validator