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

Theorem neeq12d 2739
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 2482 . 2  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
43necon3bid 2718 1  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1374    =/= wne 2655
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-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2452  df-ne 2657
This theorem is referenced by:  3netr3dOLD  2764  3netr4dOLD  2766  fnelnfp  6082  suppval  6893  infpssrlem4  8675  injresinjlem  11882  pmtr3ncom  16289  isnzr  17682  ptcmplem2  20281  axlowdimlem6  23919  axlowdimlem14  23927  usgrcyclnl1  24302  constr3lem6  24311  4cycl4dv4e  24330  usg2wotspth  24546  2spontn0vne  24549  numclwwlk2lem1  24765  numclwlk2lem2f  24766  numclwlk2lem2f1o  24768  numclwwlk5  24775  signsvvfval  28161  signsvfn  28165  derangsn  28240  derangenlem  28241  subfacp1lem3  28252  subfacp1lem5  28254  subfacp1lem6  28255  subfacp1  28256  sltval2  28979  sltres  28987  nodenselem3  29006  nodenselem5  29008  nodenselem7  29010  nofulllem4  29028  nofulllem5  29029  fvtransport  29245  stoweidlem43  31298  pgrpgt2nabl  31899  ldepsnlinc  32065  bnj1534  32865  bnj1542  32869  bnj1280  33030  cdlemkid3N  35604  cdlemkid4  35605
  Copyright terms: Public domain W3C validator