Theorem neeq1 2321

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 2146	. . 3 |- ( A = B -> ( A = C <-> B = C ) )
2	1	notbid 656	. 2 |- ( A = B -> ( -. A = C <-> -. B = C ) )
3		df-ne 2309	. 2 |- ( A =/= C <-> -. A = C )
4		df-ne 2309	. 2 |- ( B =/= C <-> -. B = C )
5	2, 3, 4	3bitr4g 222	1 |- ( A = B -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104   = wceq 1331   =/= wne 2308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-ne 2309

This theorem is referenced by:  neeq1i  2323  neeq1d  2326  nelrdva  2891  disji2  3922  0inp0  4090  frecabcl  6296  fiintim  6817  eldju2ndl  6957  updjudhf  6964  xnn0nemnf  9051  uzn0  9341  xrnemnf  9564  xrnepnf  9565  ngtmnft  9600  xsubge0  9664  xposdif  9665  xleaddadd  9670  fztpval  9863  fiinopn  12171