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 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  eqeqan12dALT  2755  funopg  6526  eqfnfv  6976  riotaeqimp  7341  soxp  8071  tfr3  8330  xpdom2  9000  dfac5lem4  10036  dfac5lem4OLD  10038  kmlem9  10069  sornom  10187  zorn2lem6  10411  elwina  10597  elina  10598  bcn1  14236  summo  15640  prodmo  15859  vdwlem12  16920  pslem  18495  gaorb  19236  gsumval3eu  19833  ringinvnz1ne0  20235  cygznlem3  21524  mat1ov  22392  dmatmulcl  22444  scmatscmiddistr  22452  scmatscm  22457  1mavmul  22492  chmatval  22773  dscmet  24516  dscopn  24517  iundisj2  25506  ltsval2  27624  wlkres  29742  wlkp1lem8  29752  1wlkdlem4  30215  frgr2wwlk1  30404  iundisj2f  32665  iundisj2fi  32877  pfxwlk  35318  erdszelem9  35393  satfv0  35552  satfv0fun  35565  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  fununiq  35963  bj-opelidb  37357  bj-ideqgALT  37363  bj-idreseq  37367  bj-idreseqb  37368  bj-ideqg1  37369  bj-ideqg1ALT  37370  unirep  37915  eqeqan2d  38438  csbfv12gALTVD  45139  fcoresf1  47315  imasetpreimafvbijlemf1  47650  prproropf1olem4  47752  paireqne  47757  prmdvdsfmtnof1lem2  47831  uspgrsprf1  48393  oppcendc  49263  discsubc  49309  euendfunc  49771  mndtcbas2  49828