Theorem neeq12d 3079

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 2839	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	3	necon3bid 3062	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ≠ wne 3018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-ne 3019

This theorem is referenced by:  2nreu  4395  fnelnfp  6941  suppval  7834  infpssrlem4  9730  injresinjlem  13160  sgrp2nmndlem5  18096  pmtr3ncom  18605  isnzr  20034  ptcmplem2  22663  isinag  26626  axlowdimlem6  26735  axlowdimlem14  26743  pthdadjvtx  27513  uhgrwkspthlem2  27537  usgr2wlkspth  27542  usgr2trlncl  27543  pthdlem1  27549  lfgrn1cycl  27585  2wlkdlem5  27710  2pthdlem1  27711  3wlkdlem5  27944  3pthdlem1  27945  numclwwlkovh0  28153  numclwwlk2lem1  28157  numclwlk2lem2f  28158  numclwlk2lem2f1o  28160  eulplig  28264  signsvvfval  31850  signsvfn  31854  bnj1534  32127  bnj1542  32131  bnj1280  32294  derangsn  32419  derangenlem  32420  subfacp1lem3  32431  subfacp1lem5  32433  subfacp1lem6  32434  subfacp1  32435  sltval2  33165  sltres  33171  noseponlem  33173  noextenddif  33177  nosepnelem  33186  nosepeq  33191  nosupbnd2lem1  33217  noetalem3  33221  fvtransport  33495  poimirlem1  34895  poimirlem6  34900  poimirlem7  34901  cdlemkid3N  38071  cdlemkid4  38072  stoweidlem43  42335  ichnreuop  43641  nnsgrpnmnd  44092  2zrngnmlid  44227  pgrpgt2nabl  44421  ldepsnlinc  44570