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

Theorem necon3ai 2959
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 2938 . . 3 𝐴𝐵𝐴 = 𝐵)
31, 2sylibr 237 . 2 (𝜑 → ¬ 𝐴𝐵)
43con2i 141 1 (𝐴𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2934
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 210  df-ne 2935
This theorem is referenced by:  necon1ai  2961  necon3i  2966  neneor  3033  nelsn  4553  disjsn2  4600  prnesn  4742  opelopabsb  5382  funsndifnop  6917  map0b  8486  mapdom3  8732  cflim2  9756  isfin4p1  9808  fpwwe2lem12  10135  tskuni  10276  recextlem2  11342  hashprg  13841  eqsqrt2d  14811  gcd1  15964  gcdzeq  15991  lcmfunsnlem2lem1  16072  lcmfunsnlem2lem2  16073  phimullem  16209  pcgcd1  16306  pc2dvds  16308  pockthlem  16334  ablfacrplem  19299  znrrg  20377  opnfbas  22586  supfil  22639  itg1addlem4  24444  itg1addlem5  24445  dvdsmulf1o  25923  ppiub  25932  dchrelbas4  25971  2sqlem8  26154  tgldimor  26440  subfacp1lem6  32710  cvmsss2  32799  ax6e2ndeq  41701  supminfxr2  42533  fourierdlem56  43229  ichnreuop  44442
  Copyright terms: Public domain W3C validator