Theorem eqeq12 2751

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  eqeqan12dALT  2753  funopg  6524  eqfnfv  6974  riotaeqimp  7339  soxp  8069  tfr3  8328  xpdom2  8998  dfac5lem4  10034  dfac5lem4OLD  10036  kmlem9  10067  sornom  10185  zorn2lem6  10409  elwina  10595  elina  10596  bcn1  14234  summo  15638  prodmo  15857  vdwlem12  16918  pslem  18493  gaorb  19234  gsumval3eu  19831  ringinvnz1ne0  20233  cygznlem3  21522  mat1ov  22390  dmatmulcl  22442  scmatscmiddistr  22450  scmatscm  22455  1mavmul  22490  chmatval  22771  dscmet  24514  dscopn  24515  iundisj2  25504  sltval2  27622  wlkres  29691  wlkp1lem8  29701  1wlkdlem4  30164  frgr2wwlk1  30353  iundisj2f  32614  iundisj2fi  32826  pfxwlk  35267  erdszelem9  35342  satfv0  35501  satfv0fun  35514  satffunlem  35544  satffunlem1lem1  35545  satffunlem2lem1  35547  fununiq  35912  bj-opelidb  37296  bj-ideqgALT  37302  bj-idreseq  37306  bj-idreseqb  37307  bj-ideqg1  37308  bj-ideqg1ALT  37309  unirep  37854  eqeqan2d  38377  csbfv12gALTVD  45081  fcoresf1  47257  imasetpreimafvbijlemf1  47592  prproropf1olem4  47694  paireqne  47699  prmdvdsfmtnof1lem2  47773  uspgrsprf1  48335  oppcendc  49205  discsubc  49251  euendfunc  49713  mndtcbas2  49770