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

Theorem neeq12d 2474
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 2472 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
3 neeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43neeq2d 2473 . 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 1632    =/= wne 2459
This theorem is referenced by:  3netr3d  2485  3netr4d  2486  infpssrlem4  7948  isnzr  16027  ptcmplem2  17763  derangsn  23716  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  subfacp1lem6  23731  subfacp1  23732  sltval2  24381  sltres  24389  nodenselem3  24408  nodenselem5  24410  nodenselem7  24412  nofulllem4  24430  nofulllem5  24431  axlowdimlem6  24647  axlowdimlem14  24655  fvtransport  24727  isnword  26089  lineval222  26182  lineval3a  26186  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  fnelnfp  26860  injresinjlem  28214  usgrcyclnl1  28386  constr3lem6  28395  4cycl4dv4e  28414  bnj1534  29201  bnj1542  29205  bnj1280  29366  cdlemkid3N  31744  cdlemkid4  31745
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator