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

Theorem mtbird 598
 Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)
Hypotheses
Ref Expression
mtbird.min (𝜑 → ¬ 𝜒)
mtbird.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtbird (𝜑 → ¬ 𝜓)

Proof of Theorem mtbird
StepHypRef Expression
1 mtbird.min . 2 (𝜑 → ¬ 𝜒)
2 mtbird.maj . . 3 (𝜑 → (𝜓𝜒))
32biimpd 132 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 589 1 (𝜑 → ¬ 𝜓)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-in1 544  ax-in2 545 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  eqneltrd  2133  neleqtrrd  2136  fidifsnen  6331  php5fin  6339  addnidpig  6434  nqnq0pi  6536  ltpopr  6693  cauappcvgprlemladdru  6754  caucvgprlemladdrl  6776  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemaddq  6806  ltposr  6848  axltirr  7086  reapirr  7568  apirr  7596  indstr2  8546  xrltnsym  8714  xrlttr  8716  xrltso  8717  lbioog  8782  ubioog  8783  fzn  8906  flqltnz  9129  expival  9257
 Copyright terms: Public domain W3C validator