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  6550  eqfnfv  7003  riotaeqimp  7370  soxp  8108  tfr3  8367  xpdom2  9036  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem9  10112  sornom  10230  zorn2lem6  10454  elwina  10639  elina  10640  bcn1  14278  summo  15683  prodmo  15902  vdwlem12  16963  pslem  18531  gaorb  19239  gsumval3eu  19834  ringinvnz1ne0  20209  cygznlem3  21479  mat1ov  22335  dmatmulcl  22387  scmatscmiddistr  22395  scmatscm  22400  1mavmul  22435  chmatval  22716  dscmet  24460  dscopn  24461  iundisj2  25450  sltval2  27568  wlkres  29598  wlkp1lem8  29608  1wlkdlem4  30069  frgr2wwlk1  30258  iundisj2f  32519  iundisj2fi  32720  pfxwlk  35111  erdszelem9  35186  satfv0  35345  satfv0fun  35358  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  fununiq  35756  bj-opelidb  37140  bj-ideqgALT  37146  bj-idreseq  37150  bj-idreseqb  37151  bj-ideqg1  37152  bj-ideqg1ALT  37153  unirep  37708  eqeqan2d  38224  csbfv12gALTVD  44888  fcoresf1  47070  imasetpreimafvbijlemf1  47405  prproropf1olem4  47507  paireqne  47512  prmdvdsfmtnof1lem2  47586  uspgrsprf1  48135  oppcendc  49007  discsubc  49053  euendfunc  49515  mndtcbas2  49572