Theorem eqeq12 2754

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 2751	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqeqan12dALT  2759  funopg  6600  eqfnfv  7051  2f1fvneq  7280  riotaeqimp  7414  soxp  8154  tfr3  8439  xpdom2  9107  dfac5lem4  10166  dfac5lem4OLD  10168  kmlem9  10199  sornom  10317  zorn2lem6  10541  elwina  10726  elina  10727  bcn1  14352  summo  15753  prodmo  15972  vdwlem12  17030  pslem  18617  gaorb  19325  gsumval3eu  19922  ringinvnz1ne0  20297  cygznlem3  21588  mat1ov  22454  dmatmulcl  22506  scmatscmiddistr  22514  scmatscm  22519  1mavmul  22554  chmatval  22835  dscmet  24585  dscopn  24586  iundisj2  25584  sltval2  27701  wlkres  29688  wlkp1lem8  29698  1wlkdlem4  30159  frgr2wwlk1  30348  iundisj2f  32603  iundisj2fi  32799  pfxwlk  35129  erdszelem9  35204  satfv0  35363  satfv0fun  35376  satffunlem  35406  satffunlem1lem1  35407  satffunlem2lem1  35409  fununiq  35769  bj-opelidb  37153  bj-ideqgALT  37159  bj-idreseq  37163  bj-idreseqb  37164  bj-ideqg1  37165  bj-ideqg1ALT  37166  unirep  37721  eqeqan2d  38237  csbfv12gALTVD  44919  fcoresf1  47081  imasetpreimafvbijlemf1  47391  prproropf1olem4  47493  paireqne  47498  prmdvdsfmtnof1lem2  47572  uspgrsprf1  48063  oppcendc  48906  mndtcbas2  49180