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

Theorem neeq12d 2838
Description: Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Hypotheses
Ref Expression
neeq1d.1 (𝜑𝐴 = 𝐵)
neeq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
neeq12d (𝜑 → (𝐴𝐶𝐵𝐷))

Proof of Theorem neeq12d
StepHypRef Expression
1 neeq1d.1 . . 3 (𝜑𝐴 = 𝐵)
2 neeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
31, 2eqeq12d 2620 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
43necon3bid 2821 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wne 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2598  df-ne 2777
This theorem is referenced by:  fnelnfp  6322  suppval  7157  infpssrlem4  8984  injresinjlem  12401  sgrp2nmndlem5  17181  pmtr3ncom  17660  isnzr  19022  ptcmplem2  21605  isinag  25443  axlowdimlem6  25541  axlowdimlem14  25549  usgrcyclnl1  25930  constr3lem6  25939  4cycl4dv4e  25958  usg2wotspth  26173  2spontn0vne  26176  numclwwlk2lem1  26391  numclwlk2lem2f  26392  numclwlk2lem2f1o  26394  numclwwlk5  26401  signsvvfval  29783  signsvfn  29787  bnj1534  29979  bnj1542  29983  bnj1280  30144  derangsn  30208  derangenlem  30209  subfacp1lem3  30220  subfacp1lem5  30222  subfacp1lem6  30223  subfacp1  30224  sltval2  30855  sltres  30863  noseponlem  30867  nodenselem3  30884  nodenselem5  30886  nodenselem7  30888  nofulllem4  30906  nofulllem5  30907  fvtransport  31111  poimirlem1  32379  poimirlem6  32384  poimirlem7  32385  cdlemkid3N  35038  cdlemkid4  35039  stoweidlem43  38736  pthdadjvtx  40934  uhgr1wlkspthlem2  40958  usgr2wlkspth  40963  usgr2trlncl  40964  pthdlem1  40970  lfgrn1cycl  41006  21wlkdlem5  41134  2pthdlem1  41135  31wlkdlem5  41328  3pthdlem1  41329  av-numclwwlk2lem1  41530  av-numclwlk2lem2f  41531  av-numclwlk2lem2f1o  41533  av-numclwwlk5  41540  nnsgrpnmnd  41606  2zrngnmlid  41737  pgrpgt2nabl  41939  ldepsnlinc  42089
  Copyright terms: Public domain W3C validator