Theorem eqeq12 2777

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  eqeqan12dALT  2779  fununiq  6560  funopg  6579  eqfnfv  7034  riotaeqimp  7407  soxp  8147  tfr3  8414  xpdom2  9098  dfac5lem4  10212  kmlem9  10244  sornom  10362  zorn2lem6  10586  elwina  10778  elina  10779  bcn1  14464  summo  15892  prodmo  16112  vdwlem12  17179  pslem  18755  gaorb  19530  gsumval3eu  20127  ringinvnz1ne0  20540  cygznlem3  21884  mat1ov  22772  dmatmulcl  22824  scmatscmiddistr  22832  scmatscm  22837  1mavmul  22872  chmatval  23156  dscmet  24900  dscopn  24901  iundisj2  25879  ltsval2  28022  brprlng  29425  wlkres  30258  wlkp1lem8  30268  pfxwlk  30275  1wlkdlem4  30740  frgr2wwlk1  30939  iundisj2f  33235  iundisj2fi  33439  erdszelem9  36054  satfv0  36213  satfv0fun  36226  satffunlem  36256  satffunlem1lem1  36257  satffunlem2lem1  36259  bj-opelidb  38182  bj-ideqgALT  38188  bj-idreseq  38192  bj-idreseqb  38193  bj-ideqg1  38194  bj-ideqg1ALT  38195  unirep  38757  eqeqan2d  39283  disjimeceqim2  39846  eldisjim3  39856  csbfv12gALTVD  45989  fcoresf1  48247  imasetpreimafvbijlemf1  48594  prproropf1olem4  48696  paireqne  48701  prmdvdsfmtnof1lem2  48778  uspgrsprf1  49353  oppcendc  50240  discsubc  50286  euendfunc  50769  mndtcobeq  50829  parhomval  50851  parhomvaln0  50861