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

Theorem necon3i 3048
Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
necon3i.1 (𝐴 = 𝐵𝐶 = 𝐷)
Assertion
Ref Expression
necon3i (𝐶𝐷𝐴𝐵)

Proof of Theorem necon3i
StepHypRef Expression
1 necon3i.1 . . 3 (𝐴 = 𝐵𝐶 = 𝐷)
21necon3ai 3041 . 2 (𝐶𝐷 → ¬ 𝐴 = 𝐵)
32neqned 3023 1 (𝐶𝐷𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  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:  difn0  4323  xpnz  6010  unixp  6127  inf3lem2  9081  infeq5  9089  cantnflem1  9141  iunfictbso  9529  rankcf  10188  hashfun  13788  hashge3el3dif  13834  abssubne0  14666  expnprm  16228  grpn0  18075  pmtr3ncomlem2  18533  pgpfaclem2  19135  isdrng2  19443  mpfrcl  20228  ply1frcl  20411  gzrngunit  20541  zringunit  20565  prmirredlem  20570  uvcf1  20866  lindfrn  20895  dfac14lem  22155  flimclslem  22522  lebnumlem3  23496  pmltpclem2  23979  i1fmullem  24224  fta1glem1  24688  fta1blem  24691  dgrcolem1  24792  plydivlem4  24814  plyrem  24823  facth  24824  fta1lem  24825  vieta1lem1  24828  vieta1lem2  24829  vieta1  24830  aalioulem2  24851  geolim3  24857  logcj  25116  argregt0  25120  argimgt0  25122  argimlt0  25123  logneg2  25125  tanarg  25129  logtayl  25170  cxpsqrt  25213  cxpcn3lem  25255  cxpcn3  25256  dcubic2  25349  dcubic  25351  cubic  25354  asinlem  25373  atandmcj  25414  atancj  25415  atanlogsublem  25420  bndatandm  25434  birthdaylem1  25457  basellem4  25589  dchrn0  25754  lgsne0  25839  usgr2trlncl  27469  nmlno0lem  28498  nmlnop0iALT  29700  eldmne0  30302  preimane  30344  cntnevol  31387  signsvtn0  31740  signstfveq0a  31746  signstfveq0  31747  nepss  32846  elima4  32917  heicant  34809  totbndbnd  34950  cdleme3c  37248  cdleme7e  37265  sn-1ne2  39038  sn-0ne2  39116  imadisjlnd  40391  compne  40653  stoweidlem39  42205  rrx2vlinest  44626  rrx2linesl  44628
  Copyright terms: Public domain W3C validator