Theorem eqeq12 2747

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqeqan12dALT  2749  funopg  6553  eqfnfv  7006  riotaeqimp  7373  soxp  8111  tfr3  8370  xpdom2  9041  dfac5lem4  10086  dfac5lem4OLD  10088  kmlem9  10119  sornom  10237  zorn2lem6  10461  elwina  10646  elina  10647  bcn1  14285  summo  15690  prodmo  15909  vdwlem12  16970  pslem  18538  gaorb  19246  gsumval3eu  19841  ringinvnz1ne0  20216  cygznlem3  21486  mat1ov  22342  dmatmulcl  22394  scmatscmiddistr  22402  scmatscm  22407  1mavmul  22442  chmatval  22723  dscmet  24467  dscopn  24468  iundisj2  25457  sltval2  27575  wlkres  29605  wlkp1lem8  29615  1wlkdlem4  30076  frgr2wwlk1  30265  iundisj2f  32526  iundisj2fi  32727  pfxwlk  35118  erdszelem9  35193  satfv0  35352  satfv0fun  35365  satffunlem  35395  satffunlem1lem1  35396  satffunlem2lem1  35398  fununiq  35763  bj-opelidb  37147  bj-ideqgALT  37153  bj-idreseq  37157  bj-idreseqb  37158  bj-ideqg1  37159  bj-ideqg1ALT  37160  unirep  37715  eqeqan2d  38231  csbfv12gALTVD  44895  fcoresf1  47074  imasetpreimafvbijlemf1  47409  prproropf1olem4  47511  paireqne  47516  prmdvdsfmtnof1lem2  47590  uspgrsprf1  48139  oppcendc  49011  discsubc  49057  euendfunc  49519  mndtcbas2  49576