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

Theorem necon3ai 2969
Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 28-Oct-2024.)
Hypothesis
Ref Expression
necon3ai.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
necon3ai (𝐴𝐵 → ¬ 𝜑)

Proof of Theorem necon3ai
StepHypRef Expression
1 neneq 2950 . 2 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
2 necon3ai.1 . 2 (𝜑𝐴 = 𝐵)
31, 2nsyl 140 1 (𝐴𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2944
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 206  df-ne 2945
This theorem is referenced by:  necon1ai  2972  necon3i  2977  neneor  3045  nelsn  4627  disjsn2  4674  prnesn  4818  opelopabsb  5488  funsndifnop  7098  ord1eln01  8443  map0b  8822  mapdom3  9094  cflim2  10200  isfin4p1  10252  fpwwe2lem12  10579  tskuni  10720  recextlem2  11787  hashprg  14296  eqsqrt2d  15254  gcd1  16409  gcdzeq  16434  lcmfunsnlem2lem1  16515  lcmfunsnlem2lem2  16516  phimullem  16652  pcgcd1  16750  pc2dvds  16752  pockthlem  16778  ablfacrplem  19845  znrrg  20975  opnfbas  23196  supfil  23249  itg1addlem4  25066  itg1addlem4OLD  25067  itg1addlem5  25068  dvdsmulf1o  26546  ppiub  26555  dchrelbas4  26594  2sqlem8  26777  tgldimor  27447  subfacp1lem6  33782  cvmsss2  33871  ax6e2ndeq  42848  supminfxr2  43711  fourierdlem56  44410  ichnreuop  45671
  Copyright terms: Public domain W3C validator