Theorem eqeq12 2753

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 2750	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 2708

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

This theorem is referenced by:  eqeqan12dALT  2755  funopg  6575  eqfnfv  7026  riotaeqimp  7393  soxp  8133  tfr3  8418  xpdom2  9086  dfac5lem4  10145  dfac5lem4OLD  10147  kmlem9  10178  sornom  10296  zorn2lem6  10520  elwina  10705  elina  10706  bcn1  14336  summo  15738  prodmo  15957  vdwlem12  17017  pslem  18587  gaorb  19295  gsumval3eu  19890  ringinvnz1ne0  20265  cygznlem3  21535  mat1ov  22391  dmatmulcl  22443  scmatscmiddistr  22451  scmatscm  22456  1mavmul  22491  chmatval  22772  dscmet  24516  dscopn  24517  iundisj2  25507  sltval2  27625  wlkres  29655  wlkp1lem8  29665  1wlkdlem4  30126  frgr2wwlk1  30315  iundisj2f  32576  iundisj2fi  32779  pfxwlk  35151  erdszelem9  35226  satfv0  35385  satfv0fun  35398  satffunlem  35428  satffunlem1lem1  35429  satffunlem2lem1  35431  fununiq  35791  bj-opelidb  37175  bj-ideqgALT  37181  bj-idreseq  37185  bj-idreseqb  37186  bj-ideqg1  37187  bj-ideqg1ALT  37188  unirep  37743  eqeqan2d  38259  csbfv12gALTVD  44890  fcoresf1  47065  imasetpreimafvbijlemf1  47385  prproropf1olem4  47487  paireqne  47492  prmdvdsfmtnof1lem2  47566  uspgrsprf1  48089  oppcendc  48960  discsubc  48998  euendfunc  49378  mndtcbas2  49427