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

Theorem mtbid 662
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 653 1  |-  ( ph  ->  -.  ch )
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 604  ax-in2 605
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylnib  666  eqneltrrd  2237  neleqtrd  2238  eueq3dc  2861  efrirr  4282  fidcenumlemrks  6848  nqnq0pi  7269  zdclt  9151  xleaddadd  9699  frec2uzf1od  10209  expnegap0  10331  bcval5  10540  zfz1isolemiso  10613  seq3coll  10616  fisumss  11192  rpdvds  11814  oddpwdclemodd  11884  pwle2  13364
  Copyright terms: Public domain W3C validator