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

Theorem necon3ai 2806
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 2785 . . 3 𝐴𝐵𝐴 = 𝐵)
31, 2sylibr 222 . 2 (𝜑 → ¬ 𝐴𝐵)
43con2i 132 1 (𝐴𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2779
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 195  df-ne 2781
This theorem is referenced by:  necon1ai  2808  necon3i  2813  neneor  2880  nelsn  4158  disjsn2  4192  opelopabsb  4899  0nelxpOLD  5057  map0b  7759  mapdom3  7994  wemapso2lem  8317  cflim2  8945  isfin4-3  8997  fpwwe2lem13  9320  tskuni  9461  recextlem2  10509  hashprg  12997  hashprgOLD  12998  eqsqrt2d  13904  gcd1  15035  gcdzeq  15057  lcmfunsnlem2lem1  15137  lcmfunsnlem2lem2  15138  phimullem  15270  pcgcd1  15367  pc2dvds  15369  pockthlem  15395  ablfacrplem  18235  znrrg  19680  opnfbas  21403  supfil  21456  itg1addlem4  23216  itg1addlem5  23217  dvdsmulf1o  24664  ppiub  24673  dchrelbas4  24712  lgsne0  24804  2sqlem8  24895  tgldimor  25141  nbcusgra  25785  uvtxnbgra  25814  wlkcpr  25850  frgraunss  26315  subfacp1lem6  30214  cvmsss2  30303  ax6e2ndeq  37579  fourierdlem56  38838  funsndifnop  40127
  Copyright terms: Public domain W3C validator