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

Theorem mtbid 646
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 637 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 588  ax-in2 589
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylnib  650  eqneltrrd  2214  neleqtrd  2215  eueq3dc  2831  efrirr  4245  fidcenumlemrks  6809  nqnq0pi  7214  zdclt  9096  xleaddadd  9638  frec2uzf1od  10147  expnegap0  10269  bcval5  10477  zfz1isolemiso  10550  seq3coll  10553  fisumss  11129  rpdvds  11707  oddpwdclemodd  11777  pwle2  13120
  Copyright terms: Public domain W3C validator