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  4398  fnelnfp  7133  2f1fvneq  7216  resf1extb  7886  suppval  8114  infpssrlem4  10228  injresinjlem  13718  sgrp2nmndlem5  18866  pmtr3ncom  19416  isnzr  20459  nzrpropd  20465  ptcmplem2  24009  ltsval2  27636  ltsres  27642  noseponlem  27644  noextenddif  27648  nosepnelem  27659  nosepeq  27665  nosupbnd2lem1  27695  noinfbnd2lem1  27710  noetasuplem4  27716  noetainflem4  27720  isinag  28922  axlowdimlem6  29032  axlowdimlem14  29040  pthdadjvtx  29813  uhgrwkspthlem2  29839  usgr2wlkspth  29844  usgr2trlncl  29845  pthdlem1  29851  lfgrn1cycl  29890  2wlkdlem5  30014  2pthdlem1  30015  3wlkdlem5  30250  3pthdlem1  30251  numclwwlkovh0  30459  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  eulplig  30572  opprqusdrng  33585  signsvvfval  34755  signsvfn  34759  bnj1534  35028  bnj1542  35032  bnj1280  35195  derangsn  35383  derangenlem  35384  subfacp1lem3  35395  subfacp1lem5  35397  subfacp1lem6  35398  subfacp1  35399  fvtransport  36245  irrdiff  37575  poimirlem1  37866  poimirlem6  37871  poimirlem7  37872  cdlemkid3N  41303  cdlemkid4  41304  aks6d1c2p2  42483  hashscontpow  42486  sticksstones1  42510  sticksstones2  42511  stoweidlem43  46395  modm1nem2  47723  ichnreuop  47826  upgrimpthslem2  48262  isubgr3stgrlem4  48323  gpg5nbgrvtx13starlem2  48426  gpgprismgr4cycllem7  48455  pgnbgreunbgrlem1  48467  pgnbgreunbgrlem4  48473  pgnbgreunbgrlem5  48477  nnsgrpnmnd  48532  2zrngnmlid  48609  pgrpgt2nabl  48720  ldepsnlinc  48862