Theorem necon3ai 2807

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 2786	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
3	1, 2	sylibr 223	. 2 ⊢ (𝜑 → ¬ 𝐴 ≠ 𝐵)
4	3	con2i 133	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon1ai  2809  necon3i  2814  neneor  2881  nelsn  4159  disjsn2  4193  opelopabsb  4910  0nelxpOLD  5068  funsndifnop  6321  map0b  7782  mapdom3  8017  wemapso2lem  8340  cflim2  8968  isfin4-3  9020  fpwwe2lem13  9343  tskuni  9484  recextlem2  10537  hashprg  13043  hashprgOLD  13044  eqsqrt2d  13956  gcd1  15087  gcdzeq  15109  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  phimullem  15322  pcgcd1  15419  pc2dvds  15421  pockthlem  15447  ablfacrplem  18287  znrrg  19733  opnfbas  21456  supfil  21509  itg1addlem4  23272  itg1addlem5  23273  dvdsmulf1o  24720  ppiub  24729  dchrelbas4  24768  lgsne0  24860  2sqlem8  24951  tgldimor  25197  nbcusgra  25992  uvtxnbgra  26021  wlkcpr  26057  frgraunss  26522  subfacp1lem6  30421  cvmsss2  30510  ax6e2ndeq  37796  fourierdlem56  39055