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

Theorem neeq12i 2615
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 2614 . 2  |-  ( A  =/=  C  <->  A  =/=  D )
3 neeq1i.1 . . 3  |-  A  =  B
43neeq1i 2613 . 2  |-  ( A  =/=  D  <->  B  =/=  D )
52, 4bitri 242 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1653    =/= wne 2601
This theorem is referenced by:  3netr3g  2631  3netr4g  2632  oppchomfval  13945  oppcbas  13949  rescbas  14034  rescco  14037  rescabs  14038  odubas  14565  oppglem  15151  mgplem  15658  mgpress  15664  opprlem  15738  sralem  16254  srasca  16258  opsrbaslem  16543  zlmsca  16807  znbaslem  16824  thlbas  16928  thlle  16929  tuslem  18302  setsmsbas  18510  setsmsds  18511  tngds  18694  zlmds  24353  zlmtset  24354  axlowdimlem6  25891  matsca  27460  hlhilslem  32812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431  df-ne 2603
  Copyright terms: Public domain W3C validator