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

Theorem mtbid 673
Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)
Hypotheses
Ref Expression
mtbid.min (𝜑 → ¬ 𝜓)
mtbid.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtbid (𝜑 → ¬ 𝜒)

Proof of Theorem mtbid
StepHypRef Expression
1 mtbid.min . 2 (𝜑 → ¬ 𝜓)
2 mtbid.maj . . 3 (𝜑 → (𝜓𝜒))
32biimprd 158 . 2 (𝜑 → (𝜒𝜓))
41, 3mtod 664 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  sylnib  677  eqneltrrd  2286  neleqtrd  2287  eueq3dc  2926  efrirr  4371  fidcenumlemrks  6982  nqnq0pi  7467  zdclt  9360  xleaddadd  9917  frec2uzf1od  10437  expnegap0  10559  bcval5  10775  zfz1isolemiso  10851  seq3coll  10854  fisumss  11432  fprodssdc  11630  rpdvds  12131  oddpwdclemodd  12204  pceq0  12354  pcmpt  12375  lgseisenlem1  14908  2sqlem8a  14927  2sqlem8  14928  pwle2  15207
  Copyright terms: Public domain W3C validator