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

Theorem neeq12i 2620
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 2619 . 2  |-  ( A  =/=  C  <->  A  =/=  D )
3 neeq1i.1 . . 3  |-  A  =  B
43neeq1i 2618 . 2  |-  ( A  =/=  D  <->  B  =/=  D )
52, 4bitri 249 1  |-  ( A  =/=  C  <->  B  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1369    =/= wne 2606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436  df-ne 2608
This theorem is referenced by:  3netr3g  2636  3netr4g  2637  oppchomfval  14653  oppcbas  14657  rescbas  14742  rescco  14745  rescabs  14746  odubas  15303  oppglem  15865  mgplem  16596  mgpress  16602  opprlem  16720  sralem  17258  srasca  17262  sravsca  17263  opsrbaslem  17559  zlmsca  17952  znbaslem  17971  thlbas  18121  thlle  18122  matsca  18316  tuslem  19842  setsmsbas  20050  setsmsds  20051  tngds  20234  ttgval  23121  ttglem  23122  cchhllem  23133  axlowdimlem6  23193  zlmds  26393  zlmtset  26394  zlmodzxzldeplem  31040  hlhilslem  35586
  Copyright terms: Public domain W3C validator