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

Theorem neeq12i 2848
 Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Hypotheses
Ref Expression
neeq1i.1 𝐴 = 𝐵
neeq12i.2 𝐶 = 𝐷
Assertion
Ref Expression
neeq12i (𝐴𝐶𝐵𝐷)

Proof of Theorem neeq12i
StepHypRef Expression
1 neeq1i.1 . . 3 𝐴 = 𝐵
2 neeq12i.2 . . 3 𝐶 = 𝐷
31, 2eqeq12i 2624 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 2834 1 (𝐴𝐶𝐵𝐷)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  3netr3g  2860  3netr4g  2861  oppchomfval  16197  oppcbas  16201  rescbas  16312  rescco  16315  rescabs  16316  odubas  16956  oppglem  17603  mgplem  18317  mgpress  18323  opprlem  18451  sralem  18998  srasca  19002  sravsca  19003  opsrbaslem  19298  opsrbaslemOLD  19299  zlmsca  19688  znbaslem  19705  znbaslemOLD  19706  thlbas  19859  thlle  19860  matsca  20040  tuslem  21881  setsmsbas  22090  setsmsds  22091  tngds  22262  ttgval  25555  ttglem  25556  cchhllem  25567  axlowdimlem6  25627  zlmds  29336  zlmtset  29337  hlhilslem  36248  zlmodzxzldeplem  42081
 Copyright terms: Public domain W3C validator