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

Theorem necon3ai 2993
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 2972 . . 3 𝐴𝐵𝐴 = 𝐵)
31, 2sylibr 226 . 2 (𝜑 → ¬ 𝐴𝐵)
43con2i 137 1 (𝐴𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1601  wne 2968
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 199  df-ne 2969
This theorem is referenced by:  necon1ai  2995  necon3i  3000  neneor  3070  nelsn  4433  disjsn2  4478  prnesn  4622  opelopabsb  5222  funsndifnop  6682  map0b  8181  mapdom3  8420  cflim2  9420  isfin4-3  9472  fpwwe2lem13  9799  tskuni  9940  recextlem2  11006  hashprg  13497  eqsqrt2d  14515  gcd1  15655  gcdzeq  15677  lcmfunsnlem2lem1  15757  lcmfunsnlem2lem2  15758  phimullem  15888  pcgcd1  15985  pc2dvds  15987  pockthlem  16013  ablfacrplem  18851  znrrg  20309  opnfbas  22054  supfil  22107  itg1addlem4  23903  itg1addlem5  23904  dvdsmulf1o  25372  ppiub  25381  dchrelbas4  25420  lgsne0  25512  2sqlem8  25603  tgldimor  25853  subfacp1lem6  31766  cvmsss2  31855  ax6e2ndeq  39701  supminfxr2  40586  fourierdlem56  41288
  Copyright terms: Public domain W3C validator