Theorem necon3ai 3012

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  necon1ai  3014  necon3i  3019  neneor  3086  nelsn  4565  disjsn2  4608  prnesn  4750  opelopabsb  5382  funsndifnop  6890  map0b  8430  mapdom3  8673  cflim2  9674  isfin4p1  9726  fpwwe2lem13  10053  tskuni  10194  recextlem2  11260  hashprg  13752  eqsqrt2d  14720  gcd1  15866  gcdzeq  15892  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  phimullem  16106  pcgcd1  16203  pc2dvds  16205  pockthlem  16231  ablfacrplem  19180  znrrg  20257  opnfbas  22447  supfil  22500  itg1addlem4  24303  itg1addlem5  24304  dvdsmulf1o  25779  ppiub  25788  dchrelbas4  25827  2sqlem8  26010  tgldimor  26296  subfacp1lem6  32545  cvmsss2  32634  ax6e2ndeq  41265  supminfxr2  42108  fourierdlem56  42804  ichnreuop  43989