Theorem necon3ai 2451

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 2403	. 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 1397   =/= wne 2402

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 2403

This theorem is referenced by:  nelsn  3704  disjsn2  3732  0nelxp  4753  fvunsng  5848  map0b  6856  difinfsnlem  7298  hashprg  11072  gcd1  12559  gcdzeq  12594  phimullem  12798  pcgcd1  12902  pc2dvds  12904  pockthlem  12930  znrrg  14676  mpodvdsmulf1o  15716  2sqlem8  15854