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 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 2732

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

This theorem is used by:  eqeqan12dALT  2779  funopg  6567  eqfnfv  7022  riotaeqimp  7396  soxp  8127  tfr3  8388  xpdom2  9070  dfac5lem4  10129  kmlem9  10161  sornom  10279  zorn2lem6  10503  elwina  10695  elina  10696  bcn1  14377  summo  15803  prodmo  16023  vdwlem12  17084  pslem  18660  gaorb  19434  gsumval3eu  20031  ringinvnz1ne0  20442  cygznlem3  21782  mat1ov  22670  dmatmulcl  22722  scmatscmiddistr  22730  scmatscm  22735  1mavmul  22770  chmatval  23054  dscmet  24798  dscopn  24799  iundisj2  25777  ltsval2  27892  brprlng  29295  wlkres  30128  wlkp1lem8  30138  pfxwlk  30145  1wlkdlem4  30610  frgr2wwlk1  30809  iundisj2f  33063  iundisj2fi  33268  erdszelem9  35778  satfv0  35937  satfv0fun  35950  satffunlem  35980  satffunlem1lem1  35981  satffunlem2lem1  35983  fununiq  36348  bj-opelidb  37904  bj-ideqgALT  37910  bj-idreseq  37914  bj-idreseqb  37915  bj-ideqg1  37916  bj-ideqg1ALT  37917  unirep  38464  eqeqan2d  38990  disjimeceqim2  39553  eldisjim3  39563  csbfv12gALTVD  45721  fcoresf1  47957  imasetpreimafvbijlemf1  48304  prproropf1olem4  48406  paireqne  48411  prmdvdsfmtnof1lem2  48488  uspgrsprf1  49063  oppcendc  49944  discsubc  49990  euendfunc  50452  mndtcbas2  50509