Theorem necon3ai 2959

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2934

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 2935

This theorem is referenced by:  necon1ai  2961  necon3i  2966  neneor  3033  nelsn  4553  disjsn2  4600  prnesn  4742  opelopabsb  5382  funsndifnop  6917  map0b  8486  mapdom3  8732  cflim2  9756  isfin4p1  9808  fpwwe2lem12  10135  tskuni  10276  recextlem2  11342  hashprg  13841  eqsqrt2d  14811  gcd1  15964  gcdzeq  15991  lcmfunsnlem2lem1  16072  lcmfunsnlem2lem2  16073  phimullem  16209  pcgcd1  16306  pc2dvds  16308  pockthlem  16334  ablfacrplem  19299  znrrg  20377  opnfbas  22586  supfil  22639  itg1addlem4  24444  itg1addlem5  24445  dvdsmulf1o  25923  ppiub  25932  dchrelbas4  25971  2sqlem8  26154  tgldimor  26440  subfacp1lem6  32710  cvmsss2  32799  ax6e2ndeq  41701  supminfxr2  42533  fourierdlem56  43229  ichnreuop  44442