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  6571  eqfnfv  7026  riotaeqimp  7394  soxp  8124  tfr3  8385  xpdom2  9059  dfac5lem4  10109  kmlem9  10141  sornom  10260  zorn2lem6  10484  elwina  10670  elina  10671  bcn1  14348  summo  15767  prodmo  15989  vdwlem12  17051  pslem  18627  gaorb  19376  gsumval3eu  19973  ringinvnz1ne0  20382  cygznlem3  21687  mat1ov  22573  dmatmulcl  22625  scmatscmiddistr  22633  scmatscm  22638  1mavmul  22673  chmatval  22954  dscmet  24697  dscopn  24698  iundisj2  25676  ltsval2  27785  brprlng  29142  wlkres  29958  wlkp1lem8  29968  1wlkdlem4  30431  frgr2wwlk1  30620  iundisj2f  32875  iundisj2fi  33082  pfxwlk  35514  erdszelem9  35589  satfv0  35748  satfv0fun  35761  satffunlem  35791  satffunlem1lem1  35792  satffunlem2lem1  35794  fununiq  36159  bj-opelidb  37683  bj-ideqgALT  37689  bj-idreseq  37693  bj-idreseqb  37694  bj-ideqg1  37695  bj-ideqg1ALT  37696  unirep  38252  eqeqan2d  38780  disjimeceqim2  39343  eldisjim3  39353  csbfv12gALTVD  45498  fcoresf1  47694  imasetpreimafvbijlemf1  48041  prproropf1olem4  48143  paireqne  48148  prmdvdsfmtnof1lem2  48225  uspgrsprf1  48800  oppcendc  49680  discsubc  49726  euendfunc  50188  mndtcbas2  50245