Theorem necomd 1635

Description: Deduction from commutative law for inequality.

Hypothesis

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

Assertion

Ref	Expression
necomd	|- (ph -> B =/= A)

Proof of Theorem necomd

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

Syntax hints:   -> wi 3   =/= wne 1583

This theorem is referenced by:  disjne 2312  ltnet 5499  xrltnet 5548  ltneOLD 5567  supxrbnd 6048  znnenlemOLD 7461  stadd 10129  strlem6 10139  hstrlem6 10147  efilcp 10504  efilcp2 10509  cnfilca 10510  dmse2 10540

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1468  df-ne 1585

Copyright terms: Public domain