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

Theorem neeq12i 2587
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 2586 . 2  |-  ( A  =/=  C  <->  A  =/=  D )
3 neeq1i.1 . . 3  |-  A  =  B
43neeq1i 2585 . 2  |-  ( A  =/=  D  <->  B  =/=  D )
52, 4bitri 241 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    =/= wne 2575
This theorem is referenced by:  3netr3g  2603  3netr4g  2604  oppchomfval  13903  oppcbas  13907  rescbas  13992  rescco  13995  rescabs  13996  odubas  14523  oppglem  15109  mgplem  15616  mgpress  15622  opprlem  15696  sralem  16212  srasca  16216  opsrbaslem  16501  zlmsca  16765  znbaslem  16782  thlbas  16886  thlle  16887  tuslem  18258  setsmsbas  18466  setsmsds  18467  tngds  18650  zlmds  24309  zlmtset  24310  axlowdimlem6  25798  matsca  27346  hlhilslem  32436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2405  df-ne 2577
  Copyright terms: Public domain W3C validator