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

Theorem necon3ai 2965
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 2946 . 2 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
2 necon3ai.1 . 2 (𝜑𝐴 = 𝐵)
31, 2nsyl 140 1 (𝐴𝐵 → ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1540  wne 2940
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 207  df-ne 2941
This theorem is referenced by:  necon1ai  2968  necon3i  2973  neneor  3042  nelsn  4666  disjsn2  4712  prnesn  4860  opelopabsb  5535  funsndifnop  7171  ord1eln01  8534  map0b  8923  mapdom3  9189  cflim2  10303  isfin4p1  10355  fpwwe2lem12  10682  tskuni  10823  recextlem2  11894  hashprg  14434  eqsqrt2d  15407  gcd1  16565  gcdzeq  16589  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  phimullem  16816  pcgcd1  16915  pc2dvds  16917  pockthlem  16943  ablfacrplem  20085  znrrg  21584  opnfbas  23850  supfil  23903  itg1addlem4  25734  itg1addlem5  25735  mpodvdsmulf1o  27237  dvdsmulf1o  27239  ppiub  27248  dchrelbas4  27287  2sqlem8  27470  tgldimor  28510  subfacp1lem6  35190  cvmsss2  35279  ax6e2ndeq  44579  supminfxr2  45480  fourierdlem56  46177  ichnreuop  47459
  Copyright terms: Public domain W3C validator