Theorem neeq1d 1591

Description: Deduction for inequality.

Hypothesis

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

Assertion

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

Proof of Theorem neeq1d

Step	Hyp	Ref	Expression
1		neeq1d.1	. 2 |- (ph -> A = B)
2		neeq1 1587	. 2 |- (A = B -> (A =/= C <-> B =/= C))
3	1, 2	syl 10	1 |- (ph -> (A =/= C <-> B =/= C))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954   =/= wne 1582

This theorem is referenced by:  fr2nr 2920  fr3nr 2921  tz7.49 3950  map0 4334  inf3lem2 4594  cplem2 4701  ac6lem 4734  kmlem12 4756  zorn2lem6 4773  recne0z 5702  recne0t 5703  expne0it 6527  elcls 7654  clsndisj 7656  elcls3 7661  islp2 7697  clslp 7698  lpbl 7832  bcthlem10 7958  bcth 7982  fine2 10411  cnfilca 10487

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467  df-ne 1584

Copyright terms: Public domain