Theorem eqeq12 2755

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  eqeqan12dALT  2760  funopg  6452  eqfnfv  6891  2f1fvneq  7114  riotaeqimp  7239  soxp  7941  tfr3  8201  xpdom2  8807  dfac5lem4  9813  kmlem9  9845  sornom  9964  zorn2lem6  10188  elwina  10373  elina  10374  bcn1  13955  summo  15357  prodmo  15574  vdwlem12  16621  pslem  18205  gaorb  18828  gsumval3eu  19420  ringinvnz1ne0  19746  cygznlem3  20689  mat1ov  21505  dmatmulcl  21557  scmatscmiddistr  21565  scmatscm  21570  1mavmul  21605  chmatval  21886  dscmet  23634  dscopn  23635  iundisj2  24618  wlkres  27940  wlkp1lem8  27950  1wlkdlem4  28405  frgr2wwlk1  28594  iundisj2f  30830  iundisj2fi  31020  pfxwlk  32985  erdszelem9  33061  satfv0  33220  satfv0fun  33233  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  fununiq  33649  sltval2  33786  bj-opelidb  35250  bj-ideqgALT  35256  bj-idreseq  35260  bj-idreseqb  35261  bj-ideqg1  35262  bj-ideqg1ALT  35263  unirep  35798  eqeqan2d  36310  csbfv12gALTVD  42408  fcoresf1  44450  imasetpreimafvbijlemf1  44744  prproropf1olem4  44846  paireqne  44851  prmdvdsfmtnof1lem2  44925  uspgrsprf1  45197  mndtcbas2  46256