Theorem neeq12d 3001

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ne 2940

This theorem is referenced by:  2nreu  4406  fnelnfp  7128  suppval  8099  infpssrlem4  10251  injresinjlem  13702  sgrp2nmndlem5  18753  pmtr3ncom  19271  isnzr  20203  ptcmplem2  23441  sltval2  27041  sltres  27047  noseponlem  27049  noextenddif  27053  nosepnelem  27064  nosepeq  27070  nosupbnd2lem1  27100  noinfbnd2lem1  27115  noetasuplem4  27121  noetainflem4  27125  isinag  27843  axlowdimlem6  27959  axlowdimlem14  27967  pthdadjvtx  28741  uhgrwkspthlem2  28765  usgr2wlkspth  28770  usgr2trlncl  28771  pthdlem1  28777  lfgrn1cycl  28813  2wlkdlem5  28937  2pthdlem1  28938  3wlkdlem5  29170  3pthdlem1  29171  numclwwlkovh0  29379  numclwwlk2lem1  29383  numclwlk2lem2f  29384  numclwlk2lem2f1o  29386  eulplig  29490  signsvvfval  33279  signsvfn  33283  bnj1534  33554  bnj1542  33558  bnj1280  33721  derangsn  33851  derangenlem  33852  subfacp1lem3  33863  subfacp1lem5  33865  subfacp1lem6  33866  subfacp1  33867  fvtransport  34693  irrdiff  35870  poimirlem1  36152  poimirlem6  36157  poimirlem7  36158  cdlemkid3N  39469  cdlemkid4  39470  aks6d1c2p2  40622  sticksstones1  40627  sticksstones2  40628  stoweidlem43  44404  ichnreuop  45784  nnsgrpnmnd  46232  2zrngnmlid  46367  pgrpgt2nabl  46562  ldepsnlinc  46709