Theorem eqeq12 2756

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqeqan12dALT  2758  funopg  6519  eqfnfv  6971  riotaeqimp  7339  soxp  8069  tfr3  8328  xpdom2  9000  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem9  10072  sornom  10190  zorn2lem6  10414  elwina  10600  elina  10601  bcn1  14266  summo  15670  prodmo  15892  vdwlem12  16954  pslem  18529  gaorb  19273  gsumval3eu  19870  ringinvnz1ne0  20272  cygznlem3  21544  mat1ov  22431  dmatmulcl  22483  scmatscmiddistr  22491  scmatscm  22496  1mavmul  22531  chmatval  22812  dscmet  24555  dscopn  24556  iundisj2  25534  ltsval2  27638  wlkres  29755  wlkp1lem8  29765  1wlkdlem4  30228  frgr2wwlk1  30417  iundisj2f  32679  iundisj2fi  32889  pfxwlk  35352  erdszelem9  35427  satfv0  35586  satfv0fun  35599  satffunlem  35629  satffunlem1lem1  35630  satffunlem2lem1  35632  fununiq  35997  bj-opelidb  37512  bj-ideqgALT  37518  bj-idreseq  37522  bj-idreseqb  37523  bj-ideqg1  37524  bj-ideqg1ALT  37525  unirep  38081  eqeqan2d  38609  disjimeceqim2  39172  eldisjim3  39182  csbfv12gALTVD  45342  fcoresf1  47532  imasetpreimafvbijlemf1  47879  prproropf1olem4  47981  paireqne  47986  prmdvdsfmtnof1lem2  48063  uspgrsprf1  48638  oppcendc  49508  discsubc  49554  euendfunc  50016  mndtcbas2  50073