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

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
StepHypRef Expression
1 necon3ai.1 . . 3 (𝜑𝐴 = 𝐵)
2 nne 2936 . . 3 𝐴𝐵𝐴 = 𝐵)
31, 2sylibr 224 . 2 (𝜑 → ¬ 𝐴𝐵)
43con2i 134 1 (𝐴𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator