Theorem neqned 2262

Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2276. One-way deduction form of df-ne 2256. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2305. (Revised by Wolf Lammen, 22-Nov-2019.)

Hypothesis

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

Assertion

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

Proof of Theorem neqned

Step	Hyp	Ref	Expression
1		neqned.1	. 2 |- ( ph -> -. A = B )
2		df-ne 2256	. 2 |- ( A =/= B <-> -. A = B )
3	1, 2	sylibr 132	1 |- ( ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1289   =/= wne 2255

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-ne 2256

This theorem is referenced by:  neqne  2263  tfr1onlemsucaccv  6088  tfrcllemsucaccv  6101  djune  6748  flqltnz  9659  zfz1iso  10210  bezoutlemle  11077  eucalgval2  11115  eucalglt  11119  lcmval  11125  lcmcllem  11129  isprm2  11179  sqne2sq  11235  nnsf  11539  peano3nninf  11541