MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3ai Structured version   Visualization version   GIF version

Theorem necon3ai 2945
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
StepHypRef Expression
1 necon3ai.1 . . 3 (𝜑𝐴 = 𝐵)
2 nne 2924 . . 3 𝐴𝐵𝐴 = 𝐵)
31, 2sylibr 224 . 2 (𝜑 → ¬ 𝐴𝐵)
43con2i 134 1 (𝐴𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1620  wne 2920
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 2921
This theorem is referenced by:  necon1ai  2947  necon3i  2952  neneor  3019  nelsn  4345  disjsn2  4379  prnesn  4526  opelopabsb  5123  0nelxpOLD  5289  funsndifnop  6567  map0b  8050  mapdom3  8285  wemapso2lem  8610  cflim2  9248  isfin4-3  9300  fpwwe2lem13  9627  tskuni  9768  recextlem2  10821  hashprg  13345  hashprgOLD  13346  eqsqrt2d  14278  gcd1  15422  gcdzeq  15444  lcmfunsnlem2lem1  15524  lcmfunsnlem2lem2  15525  phimullem  15657  pcgcd1  15754  pc2dvds  15756  pockthlem  15782  ablfacrplem  18635  znrrg  20087  opnfbas  21818  supfil  21871  itg1addlem4  23636  itg1addlem5  23637  dvdsmulf1o  25090  ppiub  25099  dchrelbas4  25138  lgsne0  25230  2sqlem8  25321  tgldimor  25567  subfacp1lem6  31445  cvmsss2  31534  ax6e2ndeq  39246  supminfxr2  40166  fourierdlem56  40851
  Copyright terms: Public domain W3C validator