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

Theorem mtbird 608
 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 136 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 599 1 (𝜑 → ¬ 𝜓)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-in1 554  ax-in2 555 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  eqneltrd  2149  neleqtrrd  2152  fidifsnen  6361  php5fin  6369  addnidpig  6491  nqnq0pi  6593  ltpopr  6750  cauappcvgprlemladdru  6811  caucvgprlemladdrl  6833  caucvgprprlemnkltj  6844  caucvgprprlemnkeqj  6845  caucvgprprlemaddq  6863  ltposr  6905  axltirr  7144  reapirr  7641  apirr  7669  indstr2  8642  xrltnsym  8814  xrlttr  8816  xrltso  8817  lbioog  8882  ubioog  8883  fzn  9007  flqltnz  9236  expival  9421  dvdsle  10155  2tp1odd  10195  oddpwdclemxy  10236  oddpwdclemndvds  10238
 Copyright terms: Public domain W3C validator