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

Theorem neeq12i 2713
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 2442 . 2  |-  ( A  =  C  <->  B  =  D )
43necon3bii 2692 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    = wceq 1437    =/= wne 2618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-ne 2620
This theorem is referenced by:  3netr3g  2731  3netr4g  2732  oppchomfval  15607  oppcbas  15611  rescbas  15722  rescco  15725  rescabs  15726  odubas  16367  oppglem  16989  mgplem  17716  mgpress  17722  opprlem  17844  sralem  18388  srasca  18392  sravsca  18393  opsrbaslem  18689  zlmsca  19079  znbaslem  19096  thlbas  19246  thlle  19247  matsca  19427  tuslem  21269  setsmsbas  21477  setsmsds  21478  tngds  21643  ttgval  24892  ttglem  24893  cchhllem  24904  axlowdimlem6  24964  zlmds  28764  zlmtset  28765  hlhilslem  35428  zlmodzxzldeplem  39565
  Copyright terms: Public domain W3C validator