Theorem necon3bid 1601

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 1599	. 2 |- (ph -> (A =/= B <-> -. C = D))
3		df-ne 1587	. 2 |- (C =/= D <-> -. C = D)
4	2, 3	syl6bbr 538	1 |- (ph -> (A =/= B <-> C =/= D))

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

This theorem is referenced by:  fodomfibOLD 4567  fodomb 4800  divne0bt 5728  expne0t 6586  expne0tOLD 6587  sqne0t 6620  cjne0t 6831  absrpclt 6855  abssubne0t 6882  georeclim 7240  mulc1cncf 7279  infxpidmlem11 7562  metgt0 7820  metne0 7821  nvgt0 8303  nv1 8304  nmorepnf 8431  nmlnogt0 8457  nmblolbii 8459  blocnilem 8464  ubthlem7 8535  ubthlem8 8536  ubthlem10 8538  normne0t 8997  normcant 9499  nmoprepnf 9794  nmfnrepnf 9807  nmlnopne0t 9924  nmophm 9961  riesz3 9995

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 1587

Copyright terms: Public domain