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

Theorem neeq12i 2618
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 2617 . 2  |-  ( A  =/=  C  <->  A  =/=  D )
3 neeq1i.1 . . 3  |-  A  =  B
43neeq1i 2616 . 2  |-  ( A  =/=  D  <->  B  =/=  D )
52, 4bitri 249 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1364    =/= wne 2604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434  df-ne 2606
This theorem is referenced by:  3netr3g  2634  3netr4g  2635  oppchomfval  14649  oppcbas  14653  rescbas  14738  rescco  14741  rescabs  14742  odubas  15299  oppglem  15858  mgplem  16586  mgpress  16592  opprlem  16710  sralem  17236  srasca  17240  sravsca  17241  opsrbaslem  17547  zlmsca  17852  znbaslem  17871  thlbas  18021  thlle  18022  matsca  18216  tuslem  19742  setsmsbas  19950  setsmsds  19951  tngds  20134  ttgval  23040  ttglem  23041  cchhllem  23052  axlowdimlem6  23112  zlmds  26313  zlmtset  26314  zlmodzxzldeplem  30864  hlhilslem  35274
  Copyright terms: Public domain W3C validator