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

Theorem mtbid 661
 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 157 . 2 (𝜑 → (𝜒𝜓))
41, 3mtod 652 1 (𝜑 → ¬ 𝜒)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  sylnib  665  eqneltrrd  2236  neleqtrd  2237  eueq3dc  2858  efrirr  4275  fidcenumlemrks  6841  nqnq0pi  7258  zdclt  9140  xleaddadd  9682  frec2uzf1od  10191  expnegap0  10313  bcval5  10521  zfz1isolemiso  10594  seq3coll  10597  fisumss  11173  rpdvds  11791  oddpwdclemodd  11861  pwle2  13277
 Copyright terms: Public domain W3C validator