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

Theorem mtbird 631
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 142 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 622 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-in1 577  ax-in2 578
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  eqneltrd  2178  neleqtrrd  2181  fidifsnen  6516  php5fin  6528  en2eqpr  6550  inflbti  6626  addnidpig  6798  nqnq0pi  6900  ltpopr  7057  cauappcvgprlemladdru  7118  caucvgprlemladdrl  7140  caucvgprprlemnkltj  7151  caucvgprprlemnkeqj  7152  caucvgprprlemaddq  7170  ltposr  7212  axltirr  7456  reapirr  7954  apirr  7982  indstr2  8991  xrltnsym  9158  xrlttr  9160  xrltso  9161  lbioog  9226  ubioog  9227  fzn  9351  flqltnz  9583  expival  9794  dvdsle  10625  2tp1odd  10664  divalglemeuneg  10703  bezoutlemle  10777  rpexp  10912  oddpwdclemxy  10927  oddpwdclemndvds  10929  sqpweven  10933  2sqpwodd  10934
  Copyright terms: Public domain W3C validator