Theorem eqeq12 2755

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 2752	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  eqeqan12dALT  2760  funopg  6468  eqfnfv  6909  2f1fvneq  7133  riotaeqimp  7259  soxp  7970  tfr3  8230  xpdom2  8854  dfac5lem4  9882  kmlem9  9914  sornom  10033  zorn2lem6  10257  elwina  10442  elina  10443  bcn1  14027  summo  15429  prodmo  15646  vdwlem12  16693  pslem  18290  gaorb  18913  gsumval3eu  19505  ringinvnz1ne0  19831  cygznlem3  20777  mat1ov  21597  dmatmulcl  21649  scmatscmiddistr  21657  scmatscm  21662  1mavmul  21697  chmatval  21978  dscmet  23728  dscopn  23729  iundisj2  24713  wlkres  28038  wlkp1lem8  28048  1wlkdlem4  28504  frgr2wwlk1  28693  iundisj2f  30929  iundisj2fi  31118  pfxwlk  33085  erdszelem9  33161  satfv0  33320  satfv0fun  33333  satffunlem  33363  satffunlem1lem1  33364  satffunlem2lem1  33366  fununiq  33743  sltval2  33859  bj-opelidb  35323  bj-ideqgALT  35329  bj-idreseq  35333  bj-idreseqb  35334  bj-ideqg1  35335  bj-ideqg1ALT  35336  unirep  35871  eqeqan2d  36383  csbfv12gALTVD  42519  fcoresf1  44563  imasetpreimafvbijlemf1  44856  prproropf1olem4  44958  paireqne  44963  prmdvdsfmtnof1lem2  45037  uspgrsprf1  45309  mndtcbas2  46370