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

Theorem neeq12i 2533
Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.)
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 neeq12i.2 . . 3  |-  C  =  D
21neeq2i 2532 . 2  |-  ( A  =/=  C  <->  A  =/=  D )
3 neeq1i.1 . . 3  |-  A  =  B
43neeq1i 2531 . 2  |-  ( A  =/=  D  <->  B  =/=  D )
52, 4bitri 240 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1642    =/= wne 2521
This theorem is referenced by:  3netr3g  2549  3netr4g  2550  oppchomfval  13716  oppcbas  13720  rescbas  13805  rescco  13808  rescabs  13809  odubas  14336  oppglem  14922  mgplem  15429  mgpress  15435  opprlem  15509  sralem  16029  srasca  16033  opsrbaslem  16318  zlmsca  16581  znbaslem  16598  thlbas  16702  thlle  16703  setsmsbas  18123  setsmsds  18124  tngds  18266  tuslem  23565  zlmds  23623  zlmtset  23624  axlowdimlem6  25134  matsca  26793  hlhilslem  32200
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2351  df-ne 2523
  Copyright terms: Public domain W3C validator