Theorem eqeq12 2757

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqeqan12dALT  2762  funopg  6612  eqfnfv  7064  2f1fvneq  7297  riotaeqimp  7431  soxp  8170  tfr3  8455  xpdom2  9133  dfac5lem4  10195  dfac5lem4OLD  10197  kmlem9  10228  sornom  10346  zorn2lem6  10570  elwina  10755  elina  10756  bcn1  14362  summo  15765  prodmo  15984  vdwlem12  17039  pslem  18642  gaorb  19347  gsumval3eu  19946  ringinvnz1ne0  20323  cygznlem3  21611  mat1ov  22475  dmatmulcl  22527  scmatscmiddistr  22535  scmatscm  22540  1mavmul  22575  chmatval  22856  dscmet  24606  dscopn  24607  iundisj2  25603  sltval2  27719  wlkres  29706  wlkp1lem8  29716  1wlkdlem4  30172  frgr2wwlk1  30361  iundisj2f  32612  iundisj2fi  32802  pfxwlk  35091  erdszelem9  35167  satfv0  35326  satfv0fun  35339  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  fununiq  35732  bj-opelidb  37118  bj-ideqgALT  37124  bj-idreseq  37128  bj-idreseqb  37129  bj-ideqg1  37130  bj-ideqg1ALT  37131  unirep  37674  eqeqan2d  38191  csbfv12gALTVD  44870  fcoresf1  46984  imasetpreimafvbijlemf1  47278  prproropf1olem4  47380  paireqne  47385  prmdvdsfmtnof1lem2  47459  uspgrsprf1  47870  mndtcbas2  48756