Theorem neeq12d 3004

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  2nreu  4372  fnelnfp  7031  suppval  7950  infpssrlem4  9993  injresinjlem  13435  sgrp2nmndlem5  18483  pmtr3ncom  18998  isnzr  20443  ptcmplem2  23112  isinag  27103  axlowdimlem6  27218  axlowdimlem14  27226  pthdadjvtx  27999  uhgrwkspthlem2  28023  usgr2wlkspth  28028  usgr2trlncl  28029  pthdlem1  28035  lfgrn1cycl  28071  2wlkdlem5  28195  2pthdlem1  28196  3wlkdlem5  28428  3pthdlem1  28429  numclwwlkovh0  28637  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  eulplig  28748  signsvvfval  32457  signsvfn  32461  bnj1534  32733  bnj1542  32737  bnj1280  32900  derangsn  33032  derangenlem  33033  subfacp1lem3  33044  subfacp1lem5  33046  subfacp1lem6  33047  subfacp1  33048  sltval2  33786  sltres  33792  noseponlem  33794  noextenddif  33798  nosepnelem  33809  nosepeq  33815  nosupbnd2lem1  33845  noinfbnd2lem1  33860  noetasuplem4  33866  noetainflem4  33870  fvtransport  34261  irrdiff  35424  poimirlem1  35705  poimirlem6  35710  poimirlem7  35711  cdlemkid3N  38874  cdlemkid4  38875  sticksstones1  40030  sticksstones2  40031  stoweidlem43  43474  ichnreuop  44812  nnsgrpnmnd  45260  2zrngnmlid  45395  pgrpgt2nabl  45590  ldepsnlinc  45737