Theorem eqeq12 2749

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

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

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  eqeqan12dALT  2754  funopg  6582  eqfnfv  7032  2f1fvneq  7258  riotaeqimp  7391  soxp  8114  tfr3  8398  xpdom2  9066  dfac5lem4  10120  kmlem9  10152  sornom  10271  zorn2lem6  10495  elwina  10680  elina  10681  bcn1  14272  summo  15662  prodmo  15879  vdwlem12  16924  pslem  18524  gaorb  19170  gsumval3eu  19771  ringinvnz1ne0  20111  cygznlem3  21124  mat1ov  21949  dmatmulcl  22001  scmatscmiddistr  22009  scmatscm  22014  1mavmul  22049  chmatval  22330  dscmet  24080  dscopn  24081  iundisj2  25065  sltval2  27156  wlkres  28924  wlkp1lem8  28934  1wlkdlem4  29390  frgr2wwlk1  29579  iundisj2f  31816  iundisj2fi  32003  pfxwlk  34109  erdszelem9  34185  satfv0  34344  satfv0fun  34357  satffunlem  34387  satffunlem1lem1  34388  satffunlem2lem1  34390  fununiq  34735  bj-opelidb  36028  bj-ideqgALT  36034  bj-idreseq  36038  bj-idreseqb  36039  bj-ideqg1  36040  bj-ideqg1ALT  36041  unirep  36577  eqeqan2d  37097  csbfv12gALTVD  43650  fcoresf1  45769  imasetpreimafvbijlemf1  46062  prproropf1olem4  46164  paireqne  46169  prmdvdsfmtnof1lem2  46243  uspgrsprf1  46515  mndtcbas2  47699