Theorem eqeq12 2754

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2729

This theorem is referenced by:  eqeqan12dALT  2759  funopg  6505  eqfnfv  6949  2f1fvneq  7173  riotaeqimp  7301  soxp  8016  tfr3  8279  xpdom2  8911  dfac5lem4  9962  kmlem9  9994  sornom  10113  zorn2lem6  10337  elwina  10522  elina  10523  bcn1  14107  summo  15508  prodmo  15725  vdwlem12  16770  pslem  18367  gaorb  18989  gsumval3eu  19580  ringinvnz1ne0  19906  cygznlem3  20860  mat1ov  21680  dmatmulcl  21732  scmatscmiddistr  21740  scmatscm  21745  1mavmul  21780  chmatval  22061  dscmet  23811  dscopn  23812  iundisj2  24796  sltval2  26887  wlkres  28174  wlkp1lem8  28184  1wlkdlem4  28640  frgr2wwlk1  28829  iundisj2f  31064  iundisj2fi  31253  pfxwlk  33224  erdszelem9  33300  satfv0  33459  satfv0fun  33472  satffunlem  33502  satffunlem1lem1  33503  satffunlem2lem1  33505  fununiq  33874  bj-opelidb  35395  bj-ideqgALT  35401  bj-idreseq  35405  bj-idreseqb  35406  bj-ideqg1  35407  bj-ideqg1ALT  35408  unirep  35943  eqeqan2d  36465  csbfv12gALTVD  42753  fcoresf1  44828  imasetpreimafvbijlemf1  45121  prproropf1olem4  45223  paireqne  45228  prmdvdsfmtnof1lem2  45302  uspgrsprf1  45574  mndtcbas2  46635