Theorem necon3bii 1601

Description: Inference from equality to inequality.

Hypothesis

Ref	Expression
necon3bii.1	⊢ (A = B ↔ C = D)

Assertion

Ref	Expression
necon3bii	⊢ (A ≠ B ↔ C ≠ D)

Proof of Theorem necon3bii

Step	Hyp	Ref	Expression
1		necon3bii.1	. . 3 ⊢ (A = B ↔ C = D)
2	1	necon3abii 1599	. 2 ⊢ (A ≠ B ↔ ¬ C = D)
3		df-ne 1590	. 2 ⊢ (C ≠ D ↔ ¬ C = D)
4	2, 3	bitr4 176	1 ⊢ (A ≠ B ↔ C ≠ D)

Syntax hints:  ¬ wn 2   ↔ wb 146   = wceq 958   ≠ wne 1588

This theorem is referenced by:  necom 1639  noinfep 4650  scott0s 4729  cplem1 4730  karden 4736  aceq5lem3 4747  negne0 5809  absgt0 6843  absdivz 6859  recvalz 6887  cjdiv 6888  abs1m 6904  abslem2i 6908  climsup 7155  cvgcmpub 7185  geoser 7234  geolimilem 7235  siii 8509  sincos4thpi 8705  bcsALT 9041  h1de2b 9472  h1de2ctlem 9473  nmlnopgt0 9917

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-ne 1590

Copyright terms: Public domain