Theorem eqeq12 2780

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		id 23	. 2 ⊢ (𝐶 = 𝐷 → 𝐶 = 𝐷)
3	1, 2	eqeqan12d 2777	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  eqeqan12dALT  2782  fununiq  6583  funopg  6602  eqfnfv  7060  riotaeqimp  7434  soxp  8178  tfr3  8445  xpdom2  9129  dfac5lem4  10244  kmlem9  10276  sornom  10394  zorn2lem6  10618  elwina  10810  elina  10811  bcn1  14498  summo  15927  prodmo  16147  vdwlem12  17214  pslem  18796  gaorb  19572  gsumval3eu  20169  ringinvnz1ne0  20582  cygznlem3  21930  mat1ov  22818  dmatmulcl  22870  scmatscmiddistr  22878  scmatscm  22883  1mavmul  22918  chmatval  23202  dscmet  24946  dscopn  24947  iundisj2  25925  ltsval2  28070  brprlng  29473  wlkres  30306  wlkp1lem8  30316  pfxwlk  30323  1wlkdlem4  30788  frgr2wwlk1  30987  iundisj2f  33282  iundisj2fi  33485  erdszelem9  36172  satfv0  36331  satfv0fun  36344  satffunlem  36374  satffunlem1lem1  36375  satffunlem2lem1  36377  bj-opelidb  38341  bj-ideqgALT  38347  bj-idreseq  38351  bj-idreseqb  38352  bj-ideqg1  38353  bj-ideqg1ALT  38354  unirep  38916  eqeqan2d  39440  disjimeceqim2  40003  eldisjim3  40013  csbfv12gALTVD  46141  fcoresf1  48412  imasetpreimafvbijlemf1  48759  prproropf1olem4  48861  paireqne  48866  prmdvdsfmtnof1lem2  48943  uspgrsprf1  49518  oppcendc  50463  discsubc  50509  euendfunc  50992  mndtcobeq  51052  parhomval  51074  parhomvaln0  51084