Theorem eqeq12 2746

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 2743	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 2701

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

This theorem is referenced by:  eqeqan12dALT  2748  funopg  6516  eqfnfv  6965  riotaeqimp  7332  soxp  8062  tfr3  8321  xpdom2  8989  dfac5lem4  10020  dfac5lem4OLD  10022  kmlem9  10053  sornom  10171  zorn2lem6  10395  elwina  10580  elina  10581  bcn1  14220  summo  15624  prodmo  15843  vdwlem12  16904  pslem  18478  gaorb  19186  gsumval3eu  19783  ringinvnz1ne0  20185  cygznlem3  21476  mat1ov  22333  dmatmulcl  22385  scmatscmiddistr  22393  scmatscm  22398  1mavmul  22433  chmatval  22714  dscmet  24458  dscopn  24459  iundisj2  25448  sltval2  27566  wlkres  29614  wlkp1lem8  29624  1wlkdlem4  30084  frgr2wwlk1  30273  iundisj2f  32534  iundisj2fi  32740  pfxwlk  35097  erdszelem9  35172  satfv0  35331  satfv0fun  35344  satffunlem  35374  satffunlem1lem1  35375  satffunlem2lem1  35377  fununiq  35742  bj-opelidb  37126  bj-ideqgALT  37132  bj-idreseq  37136  bj-idreseqb  37137  bj-ideqg1  37138  bj-ideqg1ALT  37139  unirep  37694  eqeqan2d  38210  csbfv12gALTVD  44872  fcoresf1  47053  imasetpreimafvbijlemf1  47388  prproropf1olem4  47490  paireqne  47495  prmdvdsfmtnof1lem2  47569  uspgrsprf1  48131  oppcendc  49003  discsubc  49049  euendfunc  49511  mndtcbas2  49568