Theorem neeq2d 2029

Description: Deduction for inequality.

Hypothesis

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

Assertion

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

Proof of Theorem neeq2d

Step	Hyp	Ref	Expression
1		neeq1d.1	. 2 |- (ph -> A = B)
2		neeq2 2025	. 2 |- (A = B -> (C =/= A <-> C =/= B))
3	1, 2	syl 12	1 |- (ph -> (C =/= A <-> C =/= B))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298   =/= wne 2017

This theorem is referenced by:  znnenlem 8770  eigorth 11401  eighmorth 11525  axdenselem3 14021  axdenselem5 14023  axdenselem7 14025  axfelem10 14040  axfelem15 14045  dfcon2 15442  connsub 15443  pridlval 16181  maxidlval 16187  isatlat 17012

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877  df-ne 2019

Copyright terms: Public domain