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

Theorem mtbird 597
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 588 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  2130  neleqtrrd  2133  addnidpig  6320  nqnq0pi  6421  ltpopr  6569  cauappcvgprlemladdru  6628  caucvgprlemladdrl  6649  ltposr  6691  axltirr  6883  reapirr  7361  apirr  7389  indstr2  8322  xrltnsym  8484  xrlttr  8486  xrltso  8487  lbioog  8552  ubioog  8553  fzn  8676  expival  8911
  Copyright terms: Public domain W3C validator