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

Theorem mtbid 644
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 157 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtod 635 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylnib  648  eqneltrrd  2211  neleqtrd  2212  eueq3dc  2827  efrirr  4235  fidcenumlemrks  6793  nqnq0pi  7194  zdclt  9032  xleaddadd  9563  frec2uzf1od  10072  expnegap0  10194  bcval5  10402  zfz1isolemiso  10475  seq3coll  10478  fisumss  11053  rpdvds  11626  oddpwdclemodd  11695  pwle2  12885
  Copyright terms: Public domain W3C validator