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

Theorem neeq12d 2461
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 2459 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
3 neeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43neeq2d 2460 . 2  |-  ( ph  ->  ( B  =/=  C  <->  B  =/=  D ) )
52, 4bitrd 244 1  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    =/= wne 2446
This theorem is referenced by:  3netr3d  2472  3netr4d  2473  infpssrlem4  7932  isnzr  16011  ptcmplem2  17747  derangsn  23701  derangenlem  23702  subfacp1lem3  23713  subfacp1lem5  23715  subfacp1lem6  23716  subfacp1  23717  sltval2  24310  sltres  24318  nodenselem3  24337  nodenselem5  24339  nodenselem7  24341  nofulllem4  24359  nofulllem5  24360  axlowdimlem6  24575  axlowdimlem14  24583  fvtransport  24655  isnword  25986  lineval222  26079  lineval3a  26083  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  fnelnfp  26757  bnj1534  28885  bnj1542  28889  bnj1280  29050  cdlemkid3N  31122  cdlemkid4  31123
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