Theorem necon3bid 1598

Description: Deduction from equality to inequality.

Hypothesis

Ref	Expression
necon3bid.1	|- (ph -> (A = B <-> C = D))

Assertion

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

Proof of Theorem necon3bid

Step	Hyp	Ref	Expression
1		necon3bid.1	. . 3 |- (ph -> (A = B <-> C = D))
2	1	necon3abid 1596	. 2 |- (ph -> (A =/= B <-> -. C = D))
3		df-ne 1584	. 2 |- (C =/= D <-> -. C = D)
4	2, 3	syl6bbr 537	1 |- (ph -> (A =/= B <-> C =/= D))

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

This theorem is referenced by:  fodomfib 4547  fodomb 4780  divne0bt 5699  expne0t 6526  sqne0t 6559  cjne0t 6774  absrpclt 6798  abssubne0t 6828  georeclim 7183  mulc1cncf 7222  infxpidmlem11 7513  metgt0 7772  metne0 7773  nvgt0 8255  nv1 8256  nmorepnf 8376  nmlnogt0 8402  nmblolbii 8403  blocnilem 8408  ubthlem7 8479  ubthlem8 8480  ubthlem10 8482  normne0t 8936  normcant 9439  nmoprepnf 9734  nmfnrepnf 9747  nmlnopne0t 9862  nmophm 9899  riesz3 9933

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-an 225  df-ne 1584

Copyright terms: Public domain