Theorem eqeq12 2753

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 2750	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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  eqeqan12dALT  2755  funopg  6532  eqfnfv  6983  riotaeqimp  7350  soxp  8079  tfr3  8338  xpdom2  9010  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem9  10081  sornom  10199  zorn2lem6  10423  elwina  10609  elina  10610  bcn1  14275  summo  15679  prodmo  15901  vdwlem12  16963  pslem  18538  gaorb  19282  gsumval3eu  19879  ringinvnz1ne0  20281  cygznlem3  21549  mat1ov  22413  dmatmulcl  22465  scmatscmiddistr  22473  scmatscm  22478  1mavmul  22513  chmatval  22794  dscmet  24537  dscopn  24538  iundisj2  25516  ltsval2  27620  wlkres  29737  wlkp1lem8  29747  1wlkdlem4  30210  frgr2wwlk1  30399  iundisj2f  32660  iundisj2fi  32870  pfxwlk  35306  erdszelem9  35381  satfv0  35540  satfv0fun  35553  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  fununiq  35951  bj-opelidb  37466  bj-ideqgALT  37472  bj-idreseq  37476  bj-idreseqb  37477  bj-ideqg1  37478  bj-ideqg1ALT  37479  unirep  38035  eqeqan2d  38563  disjimeceqim2  39126  eldisjim3  39136  csbfv12gALTVD  45325  fcoresf1  47517  imasetpreimafvbijlemf1  47864  prproropf1olem4  47966  paireqne  47971  prmdvdsfmtnof1lem2  48048  uspgrsprf1  48623  oppcendc  49493  discsubc  49539  euendfunc  50001  mndtcbas2  50058