Theorem necon3ai 2806

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1474   ≠ wne 2779

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 195  df-ne 2781

This theorem is referenced by:  necon1ai  2808  necon3i  2813  neneor  2880  nelsn  4158  disjsn2  4192  opelopabsb  4899  0nelxpOLD  5057  map0b  7759  mapdom3  7994  wemapso2lem  8317  cflim2  8945  isfin4-3  8997  fpwwe2lem13  9320  tskuni  9461  recextlem2  10509  hashprg  12997  hashprgOLD  12998  eqsqrt2d  13904  gcd1  15035  gcdzeq  15057  lcmfunsnlem2lem1  15137  lcmfunsnlem2lem2  15138  phimullem  15270  pcgcd1  15367  pc2dvds  15369  pockthlem  15395  ablfacrplem  18235  znrrg  19680  opnfbas  21403  supfil  21456  itg1addlem4  23216  itg1addlem5  23217  dvdsmulf1o  24664  ppiub  24673  dchrelbas4  24712  lgsne0  24804  2sqlem8  24895  tgldimor  25141  nbcusgra  25785  uvtxnbgra  25814  wlkcpr  25850  frgraunss  26315  subfacp1lem6  30214  cvmsss2  30303  ax6e2ndeq  37579  fourierdlem56  38838  funsndifnop  40127