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

Theorem neeq12i 2690
Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Hypotheses
Ref Expression
neeq1i.1  |-  A  =  B
neeq12i.2  |-  C  =  D
Assertion
Ref Expression
neeq12i  |-  ( A  =/=  C  <->  B  =/=  D )

Proof of Theorem neeq12i
StepHypRef Expression
1 neeq1i.1 . . 3  |-  A  =  B
2 neeq12i.2 . . 3  |-  C  =  D
31, 2eqeq12i 2465 . 2  |-  ( A  =  C  <->  B  =  D )
43necon3bii 2676 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    = wceq 1444    =/= wne 2622
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-cleq 2444  df-ne 2624
This theorem is referenced by:  3netr3g  2702  3netr4g  2703  oppchomfval  15619  oppcbas  15623  rescbas  15734  rescco  15737  rescabs  15738  odubas  16379  oppglem  17001  mgplem  17728  mgpress  17734  opprlem  17856  sralem  18400  srasca  18404  sravsca  18405  opsrbaslem  18701  zlmsca  19092  znbaslem  19109  thlbas  19259  thlle  19260  matsca  19440  tuslem  21282  setsmsbas  21490  setsmsds  21491  tngds  21656  ttgval  24905  ttglem  24906  cchhllem  24917  axlowdimlem6  24977  zlmds  28768  zlmtset  28769  hlhilslem  35509  zlmodzxzldeplem  40344
  Copyright terms: Public domain W3C validator