Theorem necon3ai 2426

Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)

Hypothesis

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

Assertion

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

Proof of Theorem necon3ai

Step	Hyp	Ref	Expression
1		df-ne 2378	. 2 |- ( A =/= B <-> -. A = B )
2		necon3ai.1	. . 3 |- ( ph -> A = B )
3	2	con3i 633	. 2 |- ( -. A = B -> -. ph )
4	1, 3	sylbi 121	1 |- ( A =/= B -> -. ph )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1373   =/= wne 2377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 615  ax-in2 616

This theorem depends on definitions:  df-bi 117  df-ne 2378

This theorem is referenced by:  nelsn  3673  disjsn2  3701  0nelxp  4711  fvunsng  5791  map0b  6787  difinfsnlem  7216  hashprg  10975  gcd1  12383  gcdzeq  12418  phimullem  12622  pcgcd1  12726  pc2dvds  12728  pockthlem  12754  znrrg  14497  mpodvdsmulf1o  15537  2sqlem8  15675