Theorem necon3ai 2452

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 2404	. 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 2403

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 2404

This theorem is referenced by:  nelsn  3708  disjsn2  3736  0nelxp  4759  fvunsng  5856  map0b  6899  difinfsnlem  7341  hashprg  11118  gcd1  12621  gcdzeq  12656  phimullem  12860  pcgcd1  12964  pc2dvds  12966  pockthlem  12992  znrrg  14739  mpodvdsmulf1o  15787  2sqlem8  15925