Metamath Proof Explorer

Theorem necon2bd

Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007)

Ref Expression
Hypothesis necon2bd.1 
|- ( ph -> ( ps -> A =/= B ) )
Assertion necon2bd 
|- ( ph -> ( A = B -> -. ps ) )

Proof

Step Hyp Ref Expression
1 necon2bd.1 
 |-  ( ph -> ( ps -> A =/= B ) )
2 df-ne 
 |-  ( A =/= B <-> -. A = B )
3 1 2 syl6ib 
 |-  ( ph -> ( ps -> -. A = B ) )
4 3 con2d 
 |-  ( ph -> ( A = B -> -. ps ) )