Theorem necon3ai 2424

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 2376	. 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 1372   =/= wne 2375

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 2376

This theorem is referenced by:  nelsn  3667  disjsn2  3695  0nelxp  4702  fvunsng  5777  map0b  6773  difinfsnlem  7200  hashprg  10951  gcd1  12279  gcdzeq  12314  phimullem  12518  pcgcd1  12622  pc2dvds  12624  pockthlem  12650  znrrg  14393  mpodvdsmulf1o  15433  2sqlem8  15571