Theorem neeq12d 2991

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ne 2930

This theorem is referenced by:  2nreu  4443  fnelnfp  7186  suppval  8167  infpssrlem4  10336  injresinjlem  13793  sgrp2nmndlem5  18894  pmtr3ncom  19447  isnzr  20470  ptcmplem2  24006  sltval2  27640  sltres  27646  noseponlem  27648  noextenddif  27652  nosepnelem  27663  nosepeq  27669  nosupbnd2lem1  27699  noinfbnd2lem1  27714  noetasuplem4  27720  noetainflem4  27724  isinag  28719  axlowdimlem6  28835  axlowdimlem14  28843  pthdadjvtx  29621  uhgrwkspthlem2  29645  usgr2wlkspth  29650  usgr2trlncl  29651  pthdlem1  29657  lfgrn1cycl  29693  2wlkdlem5  29817  2pthdlem1  29818  3wlkdlem5  30050  3pthdlem1  30051  numclwwlkovh0  30259  numclwwlk2lem1  30263  numclwlk2lem2f  30264  numclwlk2lem2f1o  30266  eulplig  30372  opprqusdrng  33310  signsvvfval  34343  signsvfn  34347  bnj1534  34617  bnj1542  34621  bnj1280  34784  derangsn  34913  derangenlem  34914  subfacp1lem3  34925  subfacp1lem5  34927  subfacp1lem6  34928  subfacp1  34929  fvtransport  35761  irrdiff  36938  poimirlem1  37227  poimirlem6  37232  poimirlem7  37233  cdlemkid3N  40538  cdlemkid4  40539  aks6d1c2p2  41724  hashscontpow  41727  sticksstones1  41751  sticksstones2  41752  stoweidlem43  45571  ichnreuop  46951  nnsgrpnmnd  47428  2zrngnmlid  47505  pgrpgt2nabl  47618  ldepsnlinc  47764