Theorem necon3ai 2957

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1632   ≠ wne 2932

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 197  df-ne 2933

This theorem is referenced by:  necon1ai  2959  necon3i  2964  neneor  3031  nelsn  4357  disjsn2  4391  prnesn  4538  opelopabsb  5135  0nelxpOLD  5301  funsndifnop  6580  map0b  8064  mapdom3  8299  wemapso2lem  8624  cflim2  9297  isfin4-3  9349  fpwwe2lem13  9676  tskuni  9817  recextlem2  10870  hashprg  13394  hashprgOLD  13395  eqsqrt2d  14327  gcd1  15471  gcdzeq  15493  lcmfunsnlem2lem1  15573  lcmfunsnlem2lem2  15574  phimullem  15706  pcgcd1  15803  pc2dvds  15805  pockthlem  15831  ablfacrplem  18684  znrrg  20136  opnfbas  21867  supfil  21920  itg1addlem4  23685  itg1addlem5  23686  dvdsmulf1o  25140  ppiub  25149  dchrelbas4  25188  lgsne0  25280  2sqlem8  25371  tgldimor  25617  subfacp1lem6  31495  cvmsss2  31584  ax6e2ndeq  39295  supminfxr2  40215  fourierdlem56  40900