Theorem neeq1 2433

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)

Assertion

Ref	Expression
neeq1	|- ( A = B -> ( A =/= C <-> B =/= C ) )

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		eqeq1 2245	. . 3 |- ( A = B -> ( A = C <-> B = C ) )
2	1	notbid 677	. 2 |- ( A = B -> ( -. A = C <-> -. B = C ) )
3		df-ne 2421	. 2 |- ( A =/= C <-> -. A = C )
4		df-ne 2421	. 2 |- ( B =/= C <-> -. B = C )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105   = wceq 1402   =/= wne 2420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is referenced by:  neeq1i  2435  neeq1d  2438  nelrdva  3033  disji2  4117  0inp0  4298  frecabcl  6660  fiintim  7228  eldju2ndl  7402  updjudhf  7409  netap  7610  2oneel  7612  2omotaplemap  7613  2omotaplemst  7614  exmidapne  7616  xnn0nemnf  9620  uzn0  9917  xrnemnf  10158  xrnepnf  10159  ngtmnft  10198  xsubge0  10262  xposdif  10263  xleaddadd  10268  fztpval  10468  hashdmprop2dom  11274  fun2dmnop0  11280  pcpre1  13049  pcqmul  13060  pcqcl  13063  xpsfrnel  13642  isnzr2  14464  fiinopn  15028  umgrvad2edg  16366  isclwwlk  16549  eupth2lem2dc  16614  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  3dom  16932  pw1ndom3lem  16933  qdiff  17003  neapmkv  17023  neap0mkv  17024  ltlenmkv  17025