Theorem neeq1 2413

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 2236	. . 3 |- ( A = B -> ( A = C <-> B = C ) )
2	1	notbid 671	. 2 |- ( A = B -> ( -. A = C <-> -. B = C ) )
3		df-ne 2401	. 2 |- ( A =/= C <-> -. A = C )
4		df-ne 2401	. 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 1395   =/= wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  neeq1i  2415  neeq1d  2418  nelrdva  3010  disji2  4075  0inp0  4250  frecabcl  6545  fiintim  7093  eldju2ndl  7239  updjudhf  7246  netap  7440  2oneel  7442  2omotaplemap  7443  2omotaplemst  7444  exmidapne  7446  xnn0nemnf  9443  uzn0  9738  xrnemnf  9973  xrnepnf  9974  ngtmnft  10013  xsubge0  10077  xposdif  10078  xleaddadd  10083  fztpval  10279  hashdmprop2dom  11066  fun2dmnop0  11069  pcpre1  12815  pcqmul  12826  pcqcl  12829  xpsfrnel  13377  isnzr2  14148  fiinopn  14678  umgrvad2edg  16009  neapmkv  16436  neap0mkv  16437  ltlenmkv  16438