Theorem eqeq12 2743

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 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		id 22	. 2 ⊢ (𝐶 = 𝐷 → 𝐶 = 𝐷)
3	1, 2	eqeqan12d 2740	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718

This theorem is referenced by:  eqeqan12dALT  2748  funopg  6593  eqfnfv  7044  2f1fvneq  7275  riotaeqimp  7407  soxp  8143  tfr3  8429  xpdom2  9105  dfac5lem4  10169  kmlem9  10201  sornom  10320  zorn2lem6  10544  elwina  10729  elina  10730  bcn1  14330  summo  15721  prodmo  15938  vdwlem12  16994  pslem  18597  gaorb  19301  gsumval3eu  19902  ringinvnz1ne0  20279  cygznlem3  21567  mat1ov  22441  dmatmulcl  22493  scmatscmiddistr  22501  scmatscm  22506  1mavmul  22541  chmatval  22822  dscmet  24572  dscopn  24573  iundisj2  25569  sltval2  27686  wlkres  29607  wlkp1lem8  29617  1wlkdlem4  30073  frgr2wwlk1  30262  iundisj2f  32510  iundisj2fi  32699  pfxwlk  34951  erdszelem9  35027  satfv0  35186  satfv0fun  35199  satffunlem  35229  satffunlem1lem1  35230  satffunlem2lem1  35232  fununiq  35592  bj-opelidb  36859  bj-ideqgALT  36865  bj-idreseq  36869  bj-idreseqb  36870  bj-ideqg1  36871  bj-ideqg1ALT  36872  unirep  37415  eqeqan2d  37933  csbfv12gALTVD  44575  fcoresf1  46684  imasetpreimafvbijlemf1  46976  prproropf1olem4  47078  paireqne  47083  prmdvdsfmtnof1lem2  47157  uspgrsprf1  47524  mndtcbas2  48410