Theorem necon3bii 1596

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

Syntax hints:  -. wn 2   <-> wb 146   = wceq 955   =/= wne 1583

This theorem is referenced by:  necom 1634  noinfep 4623  scott0s 4702  cplem1 4703  karden 4709  aceq5lem3 4720  negne0 5773  absdivz 6809  recvalz 6840  cjdiv 6841  abs1m 6856  abslem2i 6860  climsup 7108  cvgcmpub 7138  geoser 7186  geolimilem 7187  siii 8472  sincos4thpi 8662  bcsALT 9001  h1de2b 9432  nmlnopgt0 9878

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 1585

Copyright terms: Public domain