Theorem necon3bii 1598

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 1596	. 2 |- (A =/= B <-> -. C = D)
3		df-ne 1587	. 2 |- (C =/= D <-> -. C = D)
4	2, 3	bitr4 176	1 |- (A =/= B <-> C =/= D)

Syntax hints:  -. wn 2   <-> wb 146   = wceq 956   =/= wne 1585

This theorem is referenced by:  necom 1636  noinfep 4640  scott0s 4719  cplem1 4720  karden 4726  aceq5lem3 4737  negne0 5807  absgt0 6843  absdivz 6859  recvalz 6887  cjdiv 6888  abs1m 6904  abslem2i 6908  climsup 7155  cvgcmpub 7185  geoser 7234  geolimilem 7235  siii 8513  sincos4thpi 8710  bcsALT 9046  h1de2b 9477  h1de2ctlem 9478  nmlnopgt0 9922

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 1587

Copyright terms: Public domain