Metamath Proof Explorer

Theorem mtbii

Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995)

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

Proof

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