Theorem necon3bd 1646

Description: Contrapositive law deduction for inequality.

Hypothesis

Ref	Expression
necon3bd.1	|- (ph -> (A = B -> ps))

Assertion

Ref	Expression
necon3bd	|- (ph -> (-. ps -> A =/= B))

Proof of Theorem necon3bd

Step	Hyp	Ref	Expression
1		necon3bd.1	. . 3 |- (ph -> (A = B -> ps))
2	1	con3d 95	. 2 |- (ph -> (-. ps -> -. A = B))
3		df-ne 1630	. 2 |- (A =/= B <-> -. A = B)
4	2, 3	syl6ibr 211	1 |- (ph -> (-. ps -> A =/= B))

Syntax hints:  -. wn 2   -> wi 3   = wceq 992   =/= wne 1628

This theorem is referenced by:  peano5 3241  eceqopreq 4454  inf3lem2 4759  zneo 6371  modirr 6481  spansncvi 9875  dvrunz 10970  alexsublem2 11497  connsub 11502  filssufillem 11655  ufileulem 11657  ufileu 11658  filufint 11659  filcon 11665  flimfnfcls 11727  inficl 11849  nninfnub 11882  totbndbnd 12000

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 145  df-ne 1630

Copyright terms: Public domain