Theorem neeq12d 3029

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

Step	Hyp	Ref	Expression
1		neeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		neeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
3	1, 2	eqeq12d 2792	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	3	necon3bid 3012	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   ≠ wne 2968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2769  df-ne 2969

This theorem is referenced by:  fnelnfp  6710  suppval  7578  infpssrlem4  9463  injresinjlem  12907  sgrp2nmndlem5  17803  pmtr3ncom  18278  isnzr  19656  ptcmplem2  22265  isinag  26187  axlowdimlem6  26296  axlowdimlem14  26304  pthdadjvtx  27082  uhgrwkspthlem2  27106  usgr2wlkspth  27111  usgr2trlncl  27112  pthdlem1  27118  lfgrn1cycl  27154  2wlkdlem5  27309  2pthdlem1  27310  3wlkdlem5  27580  3pthdlem1  27581  numclwwlkovh0  27814  numclwwlk2lem1  27818  numclwlk2lem2f  27819  numclwlk2lem2f1o  27821  numclwlk2lem2fOLD  27822  numclwlk2lem2f1oOLD  27824  eulplig  27926  signsvvfval  31271  signsvfn  31275  bnj1534  31536  bnj1542  31540  bnj1280  31701  derangsn  31765  derangenlem  31766  subfacp1lem3  31777  subfacp1lem5  31779  subfacp1lem6  31780  subfacp1  31781  sltval2  32412  sltres  32418  noseponlem  32420  noextenddif  32424  nosepnelem  32433  nosepeq  32438  nosupbnd2lem1  32464  noetalem3  32468  fvtransport  32742  poimirlem1  34030  poimirlem6  34035  poimirlem7  34036  cdlemkid3N  37081  cdlemkid4  37082  stoweidlem43  41179  nnsgrpnmnd  42825  2zrngnmlid  42956  pgrpgt2nabl  43154  ldepsnlinc  43304