Theorem eqeq12 2754

Description: Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2024.)

Assertion

Ref	Expression
eqeq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Proof of Theorem eqeq12

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		id 22	. 2 ⊢ (𝐶 = 𝐷 → 𝐶 = 𝐷)
3	1, 2	eqeqan12d 2751	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542

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

This theorem is referenced by:  eqeqan12dALT  2756  funopg  6534  eqfnfv  6985  riotaeqimp  7351  soxp  8081  tfr3  8340  xpdom2  9012  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem9  10081  sornom  10199  zorn2lem6  10423  elwina  10609  elina  10610  bcn1  14248  summo  15652  prodmo  15871  vdwlem12  16932  pslem  18507  gaorb  19248  gsumval3eu  19845  ringinvnz1ne0  20247  cygznlem3  21536  mat1ov  22404  dmatmulcl  22456  scmatscmiddistr  22464  scmatscm  22469  1mavmul  22504  chmatval  22785  dscmet  24528  dscopn  24529  iundisj2  25518  ltsval2  27636  wlkres  29754  wlkp1lem8  29764  1wlkdlem4  30227  frgr2wwlk1  30416  iundisj2f  32677  iundisj2fi  32888  pfxwlk  35340  erdszelem9  35415  satfv0  35574  satfv0fun  35587  satffunlem  35617  satffunlem1lem1  35618  satffunlem2lem1  35620  fununiq  35985  bj-opelidb  37407  bj-ideqgALT  37413  bj-idreseq  37417  bj-idreseqb  37418  bj-ideqg1  37419  bj-ideqg1ALT  37420  unirep  37965  eqeqan2d  38493  disjimeceqim2  39056  eldisjim3  39066  csbfv12gALTVD  45254  fcoresf1  47429  imasetpreimafvbijlemf1  47764  prproropf1olem4  47866  paireqne  47871  prmdvdsfmtnof1lem2  47945  uspgrsprf1  48507  oppcendc  49377  discsubc  49423  euendfunc  49885  mndtcbas2  49942