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

Theorem neeq12i 3001
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 2754 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 2987 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1542  wne 2935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2731  df-ne 2936
This theorem is referenced by:  3netr3g  3013  3netr4g  3014  oppchomfval  17101  oppcbas  17105  rescbas  17217  rescco  17220  rescabs  17221  odubas  17872  oppglem  18609  mgplem  19376  mgpress  19382  opprlem  19513  sralem  20081  srasca  20085  sravsca  20086  zlmsca  20354  znbaslem  20370  thlbas  20525  thlle  20526  opsrbaslem  20873  matsca  21179  tuslem  23032  setsmsbas  23241  setsmsds  23242  tngds  23414  ttgval  26834  ttglem  26835  cchhllem  26846  axlowdimlem6  26906  zlmds  31497  zlmtset  31498  nosepne  33539  hlhilslem  39608  zlmodzxzldeplem  45421  line2  45680  prstcleval  45856  prstcocval  45858
  Copyright terms: Public domain W3C validator