Theorem neeq12d 3022

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ne 2962

This theorem is used by:  2nreu  4412  fnelnfp  7182  2f1fvneq  7265  resf1extb  7940  suppval  8167  infpssrlem4  10308  injresinjlem  13838  sgrp2nmndlem5  19022  pmtr3ncom  19576  isnzr  20648  nzrpropd  20655  ptcmplem2  24247  ltsval2  27857  ltsres  27863  noseponlem  27865  noextenddif  27869  nosepnelem  27880  nosepeq  27886  nosupbnd2lem1  27916  noinfbnd2lem1  27931  noetasuplem4  27937  noetainflem4  27941  isinag  29192  axlowdimlem6  29334  axlowdimlem14  29342  pthdadjvtx  30114  uhgrwkspthlem2  30140  usgr2wlkspth  30145  usgr2trlncl  30146  pthdlem1  30152  lfgrn1cycl  30191  2wlkdlem5  30315  2pthdlem1  30316  3wlkdlem5  30551  3pthdlem1  30552  numclwwlkovh0  30760  numclwwlk2lem1  30764  numclwlk2lem2f  30765  numclwlk2lem2f1o  30767  eulplig  30874  opprqusdrng  33806  signsvvfval  34997  signsvfn  35001  bnj1534  35273  bnj1542  35277  bnj1280  35440  derangsn  35683  derangenlem  35684  subfacp1lem3  35695  subfacp1lem5  35697  subfacp1lem6  35698  subfacp1  35699  fvtransport  36545  mh-inf3f1  37093  irrdiff  38011  poimirlem1  38313  poimirlem6  38318  poimirlem7  38319  cdlemkid3N  41748  cdlemkid4  41749  aks6d1c2p2  42927  hashscontpow  42930  sticksstones1  42954  sticksstones2  42955  stoweidlem43  46798  modm1nem2  48153  ichnreuop  48262  upgrimpthslem2  48714  isubgr3stgrlem4  48775  gpg5nbgrvtx13starlem2  48878  gpgprismgr4cycllem7  48907  pgnbgreunbgrlem1  48919  pgnbgreunbgrlem4  48925  pgnbgreunbgrlem5  48929  nnsgrpnmnd  48984  2zrngnmlid  49061  pgrpgt2nabl  49187  ldepsnlinc  49329