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

Theorem necon3ai 2807
 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 2786 . . 3 𝐴𝐵𝐴 = 𝐵)
31, 2sylibr 223 . 2 (𝜑 → ¬ 𝐴𝐵)
43con2i 133 1 (𝐴𝐵 → ¬ 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  necon1ai  2809  necon3i  2814  neneor  2881  nelsn  4159  disjsn2  4193  opelopabsb  4910  0nelxpOLD  5068  funsndifnop  6321  map0b  7782  mapdom3  8017  wemapso2lem  8340  cflim2  8968  isfin4-3  9020  fpwwe2lem13  9343  tskuni  9484  recextlem2  10537  hashprg  13043  hashprgOLD  13044  eqsqrt2d  13956  gcd1  15087  gcdzeq  15109  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  phimullem  15322  pcgcd1  15419  pc2dvds  15421  pockthlem  15447  ablfacrplem  18287  znrrg  19733  opnfbas  21456  supfil  21509  itg1addlem4  23272  itg1addlem5  23273  dvdsmulf1o  24720  ppiub  24729  dchrelbas4  24768  lgsne0  24860  2sqlem8  24951  tgldimor  25197  nbcusgra  25992  uvtxnbgra  26021  wlkcpr  26057  frgraunss  26522  subfacp1lem6  30421  cvmsss2  30510  ax6e2ndeq  37796  fourierdlem56  39055
 Copyright terms: Public domain W3C validator