Theorem eqeq12 2748

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 2745	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 2121  ax-ext 2703

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

This theorem is referenced by:  eqeqan12dALT  2750  funopg  6515  eqfnfv  6964  riotaeqimp  7329  soxp  8059  tfr3  8318  xpdom2  8985  dfac5lem4  10017  dfac5lem4OLD  10019  kmlem9  10050  sornom  10168  zorn2lem6  10392  elwina  10577  elina  10578  bcn1  14220  summo  15624  prodmo  15843  vdwlem12  16904  pslem  18478  gaorb  19219  gsumval3eu  19816  ringinvnz1ne0  20218  cygznlem3  21506  mat1ov  22363  dmatmulcl  22415  scmatscmiddistr  22423  scmatscm  22428  1mavmul  22463  chmatval  22744  dscmet  24487  dscopn  24488  iundisj2  25477  sltval2  27595  wlkres  29647  wlkp1lem8  29657  1wlkdlem4  30120  frgr2wwlk1  30309  iundisj2f  32570  iundisj2fi  32779  pfxwlk  35168  erdszelem9  35243  satfv0  35402  satfv0fun  35415  satffunlem  35445  satffunlem1lem1  35446  satffunlem2lem1  35448  fununiq  35813  bj-opelidb  37194  bj-ideqgALT  37200  bj-idreseq  37204  bj-idreseqb  37205  bj-ideqg1  37206  bj-ideqg1ALT  37207  unirep  37762  eqeqan2d  38278  csbfv12gALTVD  44939  fcoresf1  47108  imasetpreimafvbijlemf1  47443  prproropf1olem4  47545  paireqne  47550  prmdvdsfmtnof1lem2  47624  uspgrsprf1  48186  oppcendc  49058  discsubc  49104  euendfunc  49566  mndtcbas2  49623