Metamath Proof Explorer

Theorem mtbid

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995)

Ref Expression
Hypotheses mtbid.min 
|- ( ph -> -. ps )
mtbid.maj 
|- ( ph -> ( ps <-> ch ) )
Assertion mtbid 
|- ( ph -> -. ch )

Proof

Step Hyp Ref Expression
1 mtbid.min 
 |-  ( ph -> -. ps )
2 mtbid.maj 
 |-  ( ph -> ( ps <-> ch ) )
3 2 biimprd 
 |-  ( ph -> ( ch -> ps ) )
4 1 3 mtod 
 |-  ( ph -> -. ch )