Theorem eqeq12 2786

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		id 23	. 2 ⊢ (𝐶 = 𝐷 → 𝐶 = 𝐷)
3	1, 2	eqeqan12d 2783	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqeqan12dALT  2788  funopg  6568  eqfnfv  7023  riotaeqimp  7391  soxp  8121  tfr3  8382  xpdom2  9056  dfac5lem4  10106  kmlem9  10138  sornom  10257  zorn2lem6  10481  elwina  10667  elina  10668  bcn1  14345  summo  15764  prodmo  15986  vdwlem12  17048  pslem  18624  gaorb  19373  gsumval3eu  19970  ringinvnz1ne0  20379  cygznlem3  21684  mat1ov  22570  dmatmulcl  22622  scmatscmiddistr  22630  scmatscm  22635  1mavmul  22670  chmatval  22951  dscmet  24694  dscopn  24695  iundisj2  25673  ltsval2  27782  brprlng  29139  wlkres  29955  wlkp1lem8  29965  1wlkdlem4  30428  frgr2wwlk1  30617  iundisj2f  32872  iundisj2fi  33079  pfxwlk  35511  erdszelem9  35586  satfv0  35745  satfv0fun  35758  satffunlem  35788  satffunlem1lem1  35789  satffunlem2lem1  35791  fununiq  36156  bj-opelidb  37679  bj-ideqgALT  37685  bj-idreseq  37689  bj-idreseqb  37690  bj-ideqg1  37691  bj-ideqg1ALT  37692  unirep  38248  eqeqan2d  38776  disjimeceqim2  39339  eldisjim3  39349  csbfv12gALTVD  45494  fcoresf1  47690  imasetpreimafvbijlemf1  48037  prproropf1olem4  48139  paireqne  48144  prmdvdsfmtnof1lem2  48221  uspgrsprf1  48796  oppcendc  49676  discsubc  49722  euendfunc  50184  mndtcbas2  50241