Theorem neeq12d 3008

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1550   ≠ wne 2947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744  df-ne 2948

This theorem is referenced by:  2nreu  4388  fnelnfp  7146  2f1fvneq  7229  resf1extb  7900  suppval  8126  infpssrlem4  10249  injresinjlem  13782  sgrp2nmndlem5  18938  pmtr3ncom  19487  isnzr  20532  nzrpropd  20538  ptcmplem2  24082  ltsval2  27686  ltsres  27692  noseponlem  27694  noextenddif  27698  nosepnelem  27709  nosepeq  27715  nosupbnd2lem1  27745  noinfbnd2lem1  27760  noetasuplem4  27766  noetainflem4  27770  isinag  28973  axlowdimlem6  29083  axlowdimlem14  29091  pthdadjvtx  29863  uhgrwkspthlem2  29889  usgr2wlkspth  29894  usgr2trlncl  29895  pthdlem1  29901  lfgrn1cycl  29940  2wlkdlem5  30064  2pthdlem1  30065  3wlkdlem5  30300  3pthdlem1  30301  numclwwlkovh0  30509  numclwwlk2lem1  30513  numclwlk2lem2f  30514  numclwlk2lem2f1o  30516  eulplig  30623  opprqusdrng  33625  signsvvfval  34819  signsvfn  34823  bnj1534  35095  bnj1542  35099  bnj1280  35262  derangsn  35458  derangenlem  35459  subfacp1lem3  35470  subfacp1lem5  35472  subfacp1lem6  35473  subfacp1  35474  fvtransport  36320  mh-inf3f1  36839  irrdiff  37756  poimirlem1  38058  poimirlem6  38063  poimirlem7  38064  cdlemkid3N  41495  cdlemkid4  41496  aks6d1c2p2  42674  hashscontpow  42677  sticksstones1  42701  sticksstones2  42702  stoweidlem43  46555  modm1nem2  47907  ichnreuop  48016  upgrimpthslem2  48468  isubgr3stgrlem4  48529  gpg5nbgrvtx13starlem2  48632  gpgprismgr4cycllem7  48661  pgnbgreunbgrlem1  48673  pgnbgreunbgrlem4  48679  pgnbgreunbgrlem5  48683  nnsgrpnmnd  48738  2zrngnmlid  48815  pgrpgt2nabl  48926  ldepsnlinc  49068