Theorem necon3ai 2449

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1395   =/= wne 2400

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

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

This theorem is referenced by:  nelsn  3701  disjsn2  3729  0nelxp  4746  fvunsng  5832  map0b  6832  difinfsnlem  7262  hashprg  11025  gcd1  12503  gcdzeq  12538  phimullem  12742  pcgcd1  12846  pc2dvds  12848  pockthlem  12874  znrrg  14618  mpodvdsmulf1o  15658  2sqlem8  15796