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

Theorem mtbid 632
Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)
Hypotheses
Ref Expression
mtbid.min  |-  ( ph  ->  -.  ps )
mtbid.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mtbid  |-  ( ph  ->  -.  ch )

Proof of Theorem mtbid
StepHypRef Expression
1 mtbid.min . 2  |-  ( ph  ->  -.  ps )
2 mtbid.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimprd 156 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtod 624 1  |-  ( ph  ->  -.  ch )
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-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sylnib  636  eqneltrrd  2184  neleqtrd  2185  eueq3dc  2787  efrirr  4171  fidcenumlemrks  6641  nqnq0pi  6976  zdclt  8794  frec2uzf1od  9778  expnegap0  9928  ibcval5  10136  zfz1isolemiso  10209  iseqcoll  10212  fisumss  10748  rpdvds  11174  oddpwdclemodd  11243
  Copyright terms: Public domain W3C validator