Theorem eqeq12 2778

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  eqeqan12dALT  2780  funopg  6572  eqfnfv  7027  riotaeqimp  7401  soxp  8139  tfr3  8400  xpdom2  9084  dfac5lem4  10198  kmlem9  10230  sornom  10348  zorn2lem6  10572  elwina  10764  elina  10765  bcn1  14450  summo  15876  prodmo  16096  vdwlem12  17163  pslem  18739  gaorb  19514  gsumval3eu  20111  ringinvnz1ne0  20524  cygznlem3  21868  mat1ov  22756  dmatmulcl  22808  scmatscmiddistr  22816  scmatscm  22821  1mavmul  22856  chmatval  23140  dscmet  24884  dscopn  24885  iundisj2  25863  ltsval2  28006  brprlng  29409  wlkres  30242  wlkp1lem8  30252  pfxwlk  30259  1wlkdlem4  30724  frgr2wwlk1  30923  iundisj2f  33177  iundisj2fi  33382  erdszelem9  35943  satfv0  36102  satfv0fun  36115  satffunlem  36145  satffunlem1lem1  36146  satffunlem2lem1  36148  fununiq  36513  bj-opelidb  38053  bj-ideqgALT  38059  bj-idreseq  38063  bj-idreseqb  38064  bj-ideqg1  38065  bj-ideqg1ALT  38066  unirep  38628  eqeqan2d  39154  disjimeceqim2  39717  eldisjim3  39727  csbfv12gALTVD  45866  fcoresf1  48108  imasetpreimafvbijlemf1  48455  prproropf1olem4  48557  paireqne  48562  prmdvdsfmtnof1lem2  48639  uspgrsprf1  49214  oppcendc  50095  discsubc  50141  euendfunc  50603  mndtcobeq  50660