Theorem necon3ai 2461

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 2413	. 2 |- ( A =/= B <-> -. A = B )
2		necon3ai.1	. . 3 |- ( ph -> A = B )
3	2	con3i 637	. 2 |- ( -. A = B -> -. ph )
4	1, 3	sylbi 121	1 |- ( A =/= B -> -. ph )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1398   =/= wne 2412

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

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

This theorem is referenced by:  nelsn  3724  disjsn2  3752  0nelxp  4777  fvunsng  5878  map0b  6921  difinfsnlem  7390  hashprg  11173  gcd1  12683  gcdzeq  12718  phimullem  12922  pcgcd1  13026  pc2dvds  13028  pockthlem  13054  znrrg  14808  mpodvdsmulf1o  15858  2sqlem8  15996