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

Theorem neeq12d 2623
Description: Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
Hypotheses
Ref Expression
neeq1d.1  |-  ( ph  ->  A  =  B )
neeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
neeq12d  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  D ) )

Proof of Theorem neeq12d
StepHypRef Expression
1 neeq1d.1 . . 3  |-  ( ph  ->  A  =  B )
21neeq1d 2621 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
3 neeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43neeq2d 2622 . 2  |-  ( ph  ->  ( B  =/=  C  <->  B  =/=  D ) )
52, 4bitrd 253 1  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> 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:  3netr3d  2634  3netr4d  2635  fnelnfp  5908  suppval  6692  infpssrlem4  8475  injresinjlem  11638  pmtr3ncom  15981  isnzr  17341  ptcmplem2  19625  axlowdimlem6  23193  axlowdimlem14  23201  usgrcyclnl1  23526  constr3lem6  23535  4cycl4dv4e  23554  signsvvfval  26979  signsvfn  26983  derangsn  27058  derangenlem  27059  subfacp1lem3  27070  subfacp1lem5  27072  subfacp1lem6  27073  subfacp1  27074  sltval2  27797  sltres  27805  nodenselem3  27824  nodenselem5  27826  nodenselem7  27828  nofulllem4  27846  nofulllem5  27847  fvtransport  28063  stoweidlem43  29838  usg2wotspth  30403  2spontn0vne  30406  numclwwlk2lem1  30695  numclwlk2lem2f  30696  numclwlk2lem2f1o  30698  numclwwlk5  30705  pgrpgt2nabel  30769  ldepsnlinc  31050  bnj1534  31846  bnj1542  31850  bnj1280  32011  cdlemkid3N  34577  cdlemkid4  34578
  Copyright terms: Public domain W3C validator