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

Theorem neeq12d 2565
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 2563 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
3 neeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43neeq2d 2564 . 2  |-  ( ph  ->  ( B  =/=  C  <->  B  =/=  D ) )
52, 4bitrd 245 1  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    =/= wne 2550
This theorem is referenced by:  3netr3d  2576  3netr4d  2577  infpssrlem4  8119  injresinjlem  11126  isnzr  16257  ptcmplem2  18005  usgrcyclnl1  21475  constr3lem6  21484  4cycl4dv4e  21503  derangsn  24635  derangenlem  24636  subfacp1lem3  24647  subfacp1lem5  24649  subfacp1lem6  24650  subfacp1  24651  sltval2  25334  sltres  25342  nodenselem3  25361  nodenselem5  25363  nodenselem7  25365  nofulllem4  25383  nofulllem5  25384  axlowdimlem6  25600  axlowdimlem14  25608  fvtransport  25680  fnelnfp  26429  stoweidlem43  27460  bnj1534  28562  bnj1542  28566  bnj1280  28727  cdlemkid3N  31047  cdlemkid4  31048
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2380  df-ne 2552
  Copyright terms: Public domain W3C validator