ILE Home 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  6309  php5fin  6317  addnidpig  6406  nqnq0pi  6508  ltpopr  6665  cauappcvgprlemladdru  6726  caucvgprlemladdrl  6748  caucvgprprlemnkltj  6759  caucvgprprlemnkeqj  6760  caucvgprprlemaddq  6778  ltposr  6820  axltirr  7057  reapirr  7535  apirr  7563  indstr2  8509  xrltnsym  8672  xrlttr  8674  xrltso  8675  lbioog  8740  ubioog  8741  fzn  8864  expival  9126
  Copyright terms: Public domain W3C validator