Metamath Proof Explorer

Theorem necon1ad

Description: Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007) (Proof shortened by Wolf Lammen, 23-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 necon1ad.1 
 |-  ( ph -> ( -. ps -> A = B ) )
2 1 necon3ad 
 |-  ( ph -> ( A =/= B -> -. -. ps ) )
3 notnotr 
 |-  ( -. -. ps -> ps )
4 2 3 syl6 
 |-  ( ph -> ( A =/= B -> ps ) )