Theorem necon3bd 2039

Description: Contrapositive law deduction for inequality. (The proof was shortened by Andrew Salmon, 25-May-2011.)

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		nne 2021	. . 3 |- (-. A =/= B <-> A = B)
3	1, 2	syl5ib 223	. 2 |- (ph -> (-. A =/= B -> ps))
4	3	con1d 109	1 |- (ph -> (-. ps -> A =/= B))

Syntax hints:  -. wn 2   -> wi 3   = wceq 1298   =/= wne 2017

This theorem is referenced by:  nelne 2100  disjne 2919  difsn 3125  peano5 3975  eceqopreq 5372  inf3lem2 5720  zneo 7412  modirr 7522  dvrunz 10419  spansncvi 11232  atcvatlem 11957  mdsymlem3 11977  alexsublem2 15438  connsub 15443  filssufillem 15570  ufileulem 15572  ufileu 15573  filufint 15574  filcon 15580  flimfnfcls 15615  inficl 15757  nninfnub 15819  totbndbnd 15944  pm13.14 16370  atomnlej1 17030  atomnlej2 17031  hl2atom 17053  paddasslem5 17285  osumcllem4 17367  pexmidlem1 17378

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 164  df-ne 2019

Copyright terms: Public domain