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

Theorem neeq12d 2621
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 2619 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
3 neeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43neeq2d 2620 . 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 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:  3netr3d  2632  3netr4d  2633  fnelnfp  5905  suppval  6691  infpssrlem4  8471  injresinjlem  11634  pmtr3ncom  15974  isnzr  17319  ptcmplem2  19525  axlowdimlem6  23112  axlowdimlem14  23120  usgrcyclnl1  23445  constr3lem6  23454  4cycl4dv4e  23473  signsvvfval  26893  signsvfn  26897  derangsn  26972  derangenlem  26973  subfacp1lem3  26984  subfacp1lem5  26986  subfacp1lem6  26987  subfacp1  26988  sltval2  27710  sltres  27718  nodenselem3  27737  nodenselem5  27739  nodenselem7  27741  nofulllem4  27759  nofulllem5  27760  fvtransport  27976  stoweidlem43  29747  usg2wotspth  30312  2spontn0vne  30315  numclwwlk2lem1  30604  numclwlk2lem2f  30605  numclwlk2lem2f1o  30607  numclwwlk5  30614  pgrpgt2nabel  30669  ldepsnlinc  30874  bnj1534  31663  bnj1542  31667  bnj1280  31828  cdlemkid3N  34265  cdlemkid4  34266
  Copyright terms: Public domain W3C validator