Theorem neeq12d 3077

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017

This theorem is referenced by:  2nreu  4392  fnelnfp  6933  suppval  7826  infpssrlem4  9722  injresinjlem  13151  sgrp2nmndlem5  18088  pmtr3ncom  18597  isnzr  20026  ptcmplem2  22655  isinag  26618  axlowdimlem6  26727  axlowdimlem14  26735  pthdadjvtx  27505  uhgrwkspthlem2  27529  usgr2wlkspth  27534  usgr2trlncl  27535  pthdlem1  27541  lfgrn1cycl  27577  2wlkdlem5  27702  2pthdlem1  27703  3wlkdlem5  27936  3pthdlem1  27937  numclwwlkovh0  28145  numclwwlk2lem1  28149  numclwlk2lem2f  28150  numclwlk2lem2f1o  28152  eulplig  28256  signsvvfval  31843  signsvfn  31847  bnj1534  32120  bnj1542  32124  bnj1280  32287  derangsn  32412  derangenlem  32413  subfacp1lem3  32424  subfacp1lem5  32426  subfacp1lem6  32427  subfacp1  32428  sltval2  33158  sltres  33164  noseponlem  33166  noextenddif  33170  nosepnelem  33179  nosepeq  33184  nosupbnd2lem1  33210  noetalem3  33214  fvtransport  33488  poimirlem1  34887  poimirlem6  34892  poimirlem7  34893  cdlemkid3N  38063  cdlemkid4  38064  stoweidlem43  42322  ichnreuop  43628  nnsgrpnmnd  44079  2zrngnmlid  44214  pgrpgt2nabl  44408  ldepsnlinc  44557