Theorem eqeq12 2747

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

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

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqeqan12dALT  2752  funopg  6581  eqfnfv  7031  2f1fvneq  7261  riotaeqimp  7394  soxp  8117  tfr3  8401  xpdom2  9069  dfac5lem4  10123  kmlem9  10155  sornom  10274  zorn2lem6  10498  elwina  10683  elina  10684  bcn1  14277  summo  15667  prodmo  15884  vdwlem12  16929  pslem  18529  gaorb  19212  gsumval3eu  19813  ringinvnz1ne0  20188  cygznlem3  21344  mat1ov  22170  dmatmulcl  22222  scmatscmiddistr  22230  scmatscm  22235  1mavmul  22270  chmatval  22551  dscmet  24301  dscopn  24302  iundisj2  25298  sltval2  27395  wlkres  29194  wlkp1lem8  29204  1wlkdlem4  29660  frgr2wwlk1  29849  iundisj2f  32088  iundisj2fi  32275  pfxwlk  34412  erdszelem9  34488  satfv0  34647  satfv0fun  34660  satffunlem  34690  satffunlem1lem1  34691  satffunlem2lem1  34693  fununiq  35044  bj-opelidb  36336  bj-ideqgALT  36342  bj-idreseq  36346  bj-idreseqb  36347  bj-ideqg1  36348  bj-ideqg1ALT  36349  unirep  36885  eqeqan2d  37405  csbfv12gALTVD  43962  fcoresf1  46077  imasetpreimafvbijlemf1  46370  prproropf1olem4  46472  paireqne  46477  prmdvdsfmtnof1lem2  46551  uspgrsprf1  46823  mndtcbas2  47796