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

Theorem neeq12i 2458
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 2457 . 2  |-  ( A  =/=  C  <->  A  =/=  D )
3 neeq1i.1 . . 3  |-  A  =  B
43neeq1i 2456 . 2  |-  ( A  =/=  D  <->  B  =/=  D )
52, 4bitri 240 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    =/= wne 2446
This theorem is referenced by:  3netr3g  2474  3netr4g  2475  oppchomfval  13617  oppcbas  13621  rescbas  13706  rescco  13709  rescabs  13710  odubas  14237  oppglem  14823  mgplem  15330  mgpress  15336  opprlem  15410  sralem  15930  srasca  15934  opsrbaslem  16219  zlmsca  16475  znbaslem  16492  thlbas  16596  thlle  16597  setsmsbas  18021  setsmsds  18022  tngds  18164  axlowdimlem6  24575  matsca  27470  hlhilslem  32131
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator