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

Theorem neeq12d 2720
Description: Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
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 )
2 neeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
31, 2eqeq12d 2463 . 2  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
43necon3bid 2699 1  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1381    =/= wne 2636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2433  df-ne 2638
This theorem is referenced by:  3netr3dOLD  2745  3netr4dOLD  2747  fnelnfp  6082  suppval  6901  infpssrlem4  8684  injresinjlem  11899  sgrp2nmndlem5  15916  pmtr3ncom  16369  isnzr  17775  ptcmplem2  20419  iscgra  24034  axlowdimlem6  24115  axlowdimlem14  24123  usgrcyclnl1  24505  constr3lem6  24514  4cycl4dv4e  24533  usg2wotspth  24749  2spontn0vne  24752  numclwwlk2lem1  24967  numclwlk2lem2f  24968  numclwlk2lem2f1o  24970  numclwwlk5  24977  signsvvfval  28401  signsvfn  28405  derangsn  28480  derangenlem  28481  subfacp1lem3  28492  subfacp1lem5  28494  subfacp1lem6  28495  subfacp1  28496  sltval2  29384  sltres  29392  nodenselem3  29411  nodenselem5  29413  nodenselem7  29415  nofulllem4  29433  nofulllem5  29434  fvtransport  29650  stoweidlem43  31710  nnsgrpnmnd  32339  2zrngnmlid  32455  pgrpgt2nabl  32667  ldepsnlinc  32819  bnj1534  33618  bnj1542  33622  bnj1280  33783  cdlemkid3N  36361  cdlemkid4  36362
  Copyright terms: Public domain W3C validator