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

Theorem necon3ai 3039
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 3018 . . 3 𝐴𝐵𝐴 = 𝐵)
31, 2sylibr 236 . 2 (𝜑 → ¬ 𝐴𝐵)
43con2i 141 1 (𝐴𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1530  wne 3014
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 209  df-ne 3015
This theorem is referenced by:  necon1ai  3041  necon3i  3046  neneor  3116  nelsn  4597  disjsn2  4640  prnesn  4782  opelopabsb  5408  funsndifnop  6906  map0b  8439  mapdom3  8681  cflim2  9677  isfin4p1  9729  fpwwe2lem13  10056  tskuni  10197  recextlem2  11263  hashprg  13748  eqsqrt2d  14720  gcd1  15868  gcdzeq  15894  lcmfunsnlem2lem1  15974  lcmfunsnlem2lem2  15975  phimullem  16108  pcgcd1  16205  pc2dvds  16207  pockthlem  16233  ablfacrplem  19179  znrrg  20704  opnfbas  22442  supfil  22495  itg1addlem4  24292  itg1addlem5  24293  dvdsmulf1o  25763  ppiub  25772  dchrelbas4  25811  2sqlem8  25994  tgldimor  26280  subfacp1lem6  32420  cvmsss2  32509  ax6e2ndeq  40878  supminfxr2  41729  fourierdlem56  42432  ichnreuop  43619
  Copyright terms: Public domain W3C validator