Theorem necon3ai 3043

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3018

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 3019

This theorem is referenced by:  necon1ai  3045  necon3i  3050  neneor  3120  nelsn  4607  disjsn2  4650  prnesn  4792  opelopabsb  5419  funsndifnop  6915  map0b  8449  mapdom3  8691  cflim2  9687  isfin4p1  9739  fpwwe2lem13  10066  tskuni  10207  recextlem2  11273  hashprg  13759  eqsqrt2d  14730  gcd1  15878  gcdzeq  15904  lcmfunsnlem2lem1  15984  lcmfunsnlem2lem2  15985  phimullem  16118  pcgcd1  16215  pc2dvds  16217  pockthlem  16243  ablfacrplem  19189  znrrg  20714  opnfbas  22452  supfil  22505  itg1addlem4  24302  itg1addlem5  24303  dvdsmulf1o  25773  ppiub  25782  dchrelbas4  25821  2sqlem8  26004  tgldimor  26290  subfacp1lem6  32434  cvmsss2  32523  ax6e2ndeq  40900  supminfxr2  41752  fourierdlem56  42454  ichnreuop  43641