Theorem necon3ai 2993

Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

Ref	Expression
necon3ai.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
necon3ai	⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

Proof of Theorem necon3ai

Step	Hyp	Ref	Expression
1		necon3ai.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		nne 2972	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
3	1, 2	sylibr 226	. 2 ⊢ (𝜑 → ¬ 𝐴 ≠ 𝐵)
4	3	con2i 137	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1601   ≠ wne 2968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-ne 2969

This theorem is referenced by:  necon1ai  2995  necon3i  3000  neneor  3070  nelsn  4433  disjsn2  4478  prnesn  4622  opelopabsb  5222  funsndifnop  6682  map0b  8181  mapdom3  8420  cflim2  9420  isfin4-3  9472  fpwwe2lem13  9799  tskuni  9940  recextlem2  11006  hashprg  13497  eqsqrt2d  14515  gcd1  15655  gcdzeq  15677  lcmfunsnlem2lem1  15757  lcmfunsnlem2lem2  15758  phimullem  15888  pcgcd1  15985  pc2dvds  15987  pockthlem  16013  ablfacrplem  18851  znrrg  20309  opnfbas  22054  supfil  22107  itg1addlem4  23903  itg1addlem5  23904  dvdsmulf1o  25372  ppiub  25381  dchrelbas4  25420  lgsne0  25512  2sqlem8  25603  tgldimor  25853  subfacp1lem6  31766  cvmsss2  31855  ax6e2ndeq  39701  supminfxr2  40586  fourierdlem56  41288