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

Theorem neeq12i 2732
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 2463 . 2  |-  ( A  =  C  <->  B  =  D )
43necon3bii 2711 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1383    =/= wne 2638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ne 2640
This theorem is referenced by:  3netr3g  2750  3netr4g  2751  oppchomfval  14986  oppcbas  14990  rescbas  15075  rescco  15078  rescabs  15079  odubas  15637  oppglem  16259  mgplem  17020  mgpress  17026  opprlem  17151  sralem  17697  srasca  17701  sravsca  17702  opsrbaslem  18016  zlmsca  18431  znbaslem  18450  thlbas  18600  thlle  18601  matsca  18790  tuslem  20643  setsmsbas  20851  setsmsds  20852  tngds  21035  ttgval  24050  ttglem  24051  cchhllem  24062  axlowdimlem6  24122  zlmds  27818  zlmtset  27819  zlmodzxzldeplem  32834  hlhilslem  37408
  Copyright terms: Public domain W3C validator