Theorem necon3ai 3044

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 3019

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 209  df-ne 3020

This theorem is referenced by:  necon1ai  3046  necon3i  3051  neneor  3121  nelsn  4608  disjsn2  4651  prnesn  4793  opelopabsb  5420  funsndifnop  6916  map0b  8450  mapdom3  8692  cflim2  9688  isfin4p1  9740  fpwwe2lem13  10067  tskuni  10208  recextlem2  11274  hashprg  13759  eqsqrt2d  14731  gcd1  15879  gcdzeq  15905  lcmfunsnlem2lem1  15985  lcmfunsnlem2lem2  15986  phimullem  16119  pcgcd1  16216  pc2dvds  16218  pockthlem  16244  ablfacrplem  19190  znrrg  20715  opnfbas  22453  supfil  22506  itg1addlem4  24303  itg1addlem5  24304  dvdsmulf1o  25774  ppiub  25783  dchrelbas4  25822  2sqlem8  26005  tgldimor  26291  subfacp1lem6  32436  cvmsss2  32525  ax6e2ndeq  40899  supminfxr2  41751  fourierdlem56  42454  ichnreuop  43641