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

Theorem neeq12i 2756
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 2487 . 2  |-  ( A  =  C  <->  B  =  D )
43necon3bii 2735 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1379    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664
This theorem is referenced by:  3netr3g  2774  3netr4g  2775  oppchomfval  14970  oppcbas  14974  rescbas  15059  rescco  15062  rescabs  15063  odubas  15620  oppglem  16190  mgplem  16948  mgpress  16954  opprlem  17078  sralem  17623  srasca  17627  sravsca  17628  opsrbaslem  17941  zlmsca  18353  znbaslem  18372  thlbas  18522  thlle  18523  matsca  18712  tuslem  20533  setsmsbas  20741  setsmsds  20742  tngds  20925  ttgval  23882  ttglem  23883  cchhllem  23894  axlowdimlem6  23954  zlmds  27609  zlmtset  27610  zlmodzxzldeplem  32198  hlhilslem  36756
  Copyright terms: Public domain W3C validator