Theorem neeq12d 2996

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  2nreu  4379  fnelnfp  7128  2f1fvneq  7211  resf1extb  7881  suppval  8109  infpssrlem4  10226  injresinjlem  13743  sgrp2nmndlem5  18898  pmtr3ncom  19448  isnzr  20493  nzrpropd  20499  ptcmplem2  24043  ltsval2  27645  ltsres  27651  noseponlem  27653  noextenddif  27657  nosepnelem  27668  nosepeq  27674  nosupbnd2lem1  27704  noinfbnd2lem1  27719  noetasuplem4  27725  noetainflem4  27729  isinag  28931  axlowdimlem6  29041  axlowdimlem14  29049  pthdadjvtx  29821  uhgrwkspthlem2  29847  usgr2wlkspth  29852  usgr2trlncl  29853  pthdlem1  29859  lfgrn1cycl  29898  2wlkdlem5  30022  2pthdlem1  30023  3wlkdlem5  30258  3pthdlem1  30259  numclwwlkovh0  30467  numclwwlk2lem1  30471  numclwlk2lem2f  30472  numclwlk2lem2f1o  30474  eulplig  30581  opprqusdrng  33583  signsvvfval  34769  signsvfn  34773  bnj1534  35042  bnj1542  35046  bnj1280  35209  derangsn  35405  derangenlem  35406  subfacp1lem3  35417  subfacp1lem5  35419  subfacp1lem6  35420  subfacp1  35421  fvtransport  36267  mh-inf3f1  36776  irrdiff  37693  poimirlem1  37995  poimirlem6  38000  poimirlem7  38001  cdlemkid3N  41432  cdlemkid4  41433  aks6d1c2p2  42611  hashscontpow  42614  sticksstones1  42638  sticksstones2  42639  stoweidlem43  46493  modm1nem2  47845  ichnreuop  47954  upgrimpthslem2  48406  isubgr3stgrlem4  48467  gpg5nbgrvtx13starlem2  48570  gpgprismgr4cycllem7  48599  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5  48621  nnsgrpnmnd  48676  2zrngnmlid  48753  pgrpgt2nabl  48864  ldepsnlinc  49006