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

Theorem necon3ai 3041
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 3020 . . 3 𝐴𝐵𝐴 = 𝐵)
31, 2sylibr 235 . 2 (𝜑 → ¬ 𝐴𝐵)
43con2i 141 1 (𝐴𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon1ai  3043  necon3i  3048  neneor  3118  nelsn  4597  disjsn2  4642  prnesn  4784  opelopabsb  5409  funsndifnop  6906  map0b  8437  mapdom3  8678  cflim2  9674  isfin4p1  9726  fpwwe2lem13  10053  tskuni  10194  recextlem2  11260  hashprg  13746  eqsqrt2d  14718  gcd1  15866  gcdzeq  15892  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  phimullem  16106  pcgcd1  16203  pc2dvds  16205  pockthlem  16231  ablfacrplem  19118  znrrg  20642  opnfbas  22380  supfil  22433  itg1addlem4  24229  itg1addlem5  24230  dvdsmulf1o  25699  ppiub  25708  dchrelbas4  25747  2sqlem8  25930  tgldimor  26216  subfacp1lem6  32330  cvmsss2  32419  ax6e2ndeq  40773  supminfxr2  41625  fourierdlem56  42328  ichnreuop  43481
  Copyright terms: Public domain W3C validator