Theorem neeq12d 2994

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  2nreu  4385  fnelnfp  7125  2f1fvneq  7208  resf1extb  7878  suppval  8105  infpssrlem4  10219  injresinjlem  13736  sgrp2nmndlem5  18891  pmtr3ncom  19441  isnzr  20482  nzrpropd  20488  ptcmplem2  24028  ltsval2  27634  ltsres  27640  noseponlem  27642  noextenddif  27646  nosepnelem  27657  nosepeq  27663  nosupbnd2lem1  27693  noinfbnd2lem1  27708  noetasuplem4  27714  noetainflem4  27718  isinag  28920  axlowdimlem6  29030  axlowdimlem14  29038  pthdadjvtx  29811  uhgrwkspthlem2  29837  usgr2wlkspth  29842  usgr2trlncl  29843  pthdlem1  29849  lfgrn1cycl  29888  2wlkdlem5  30012  2pthdlem1  30013  3wlkdlem5  30248  3pthdlem1  30249  numclwwlkovh0  30457  numclwwlk2lem1  30461  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  eulplig  30571  opprqusdrng  33568  signsvvfval  34738  signsvfn  34742  bnj1534  35011  bnj1542  35015  bnj1280  35178  derangsn  35368  derangenlem  35369  subfacp1lem3  35380  subfacp1lem5  35382  subfacp1lem6  35383  subfacp1  35384  fvtransport  36230  mh-inf3f1  36739  irrdiff  37656  poimirlem1  37956  poimirlem6  37961  poimirlem7  37962  cdlemkid3N  41393  cdlemkid4  41394  aks6d1c2p2  42572  hashscontpow  42575  sticksstones1  42599  sticksstones2  42600  stoweidlem43  46489  modm1nem2  47835  ichnreuop  47944  upgrimpthslem2  48396  isubgr3stgrlem4  48457  gpg5nbgrvtx13starlem2  48560  gpgprismgr4cycllem7  48589  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5  48611  nnsgrpnmnd  48666  2zrngnmlid  48743  pgrpgt2nabl  48854  ldepsnlinc  48996