Theorem eqeq12 2780

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqeqan12dALT  2782  funopg  6570  eqfnfv  7025  riotaeqimp  7393  soxp  8121  tfr3  8382  xpdom2  9056  dfac5lem4  10106  kmlem9  10138  sornom  10256  zorn2lem6  10480  elwina  10666  elina  10667  bcn1  14345  summo  15764  prodmo  15986  vdwlem12  17047  pslem  18623  gaorb  19372  gsumval3eu  19969  ringinvnz1ne0  20379  cygznlem3  21719  mat1ov  22605  dmatmulcl  22657  scmatscmiddistr  22665  scmatscm  22670  1mavmul  22705  chmatval  22986  dscmet  24729  dscopn  24730  iundisj2  25708  ltsval2  27820  brprlng  29188  wlkres  30018  wlkp1lem8  30028  1wlkdlem4  30491  frgr2wwlk1  30680  iundisj2f  32935  iundisj2fi  33142  pfxwlk  35616  erdszelem9  35691  satfv0  35850  satfv0fun  35863  satffunlem  35893  satffunlem1lem1  35894  satffunlem2lem1  35896  fununiq  36261  bj-opelidb  37796  bj-ideqgALT  37802  bj-idreseq  37806  bj-idreseqb  37807  bj-ideqg1  37808  bj-ideqg1ALT  37809  unirep  38365  eqeqan2d  38891  disjimeceqim2  39454  eldisjim3  39464  csbfv12gALTVD  45607  fcoresf1  47806  imasetpreimafvbijlemf1  48153  prproropf1olem4  48255  paireqne  48260  prmdvdsfmtnof1lem2  48337  uspgrsprf1  48912  oppcendc  49796  discsubc  49842  euendfunc  50304  mndtcbas2  50361