Metamath Proof Explorer

Theorem necomd

Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008)

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

Proof

Step Hyp Ref Expression
1 necomd.1 
 |-  ( ph -> A =/= B )
2 necom 
 |-  ( A =/= B <-> B =/= A )
3 1 2 sylib 
 |-  ( ph -> B =/= A )