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 206   ∧ wa 395   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqeqan12dALT  2756  funopg  6527  eqfnfv  6978  riotaeqimp  7344  soxp  8073  tfr3  8332  xpdom2  9004  dfac5lem4  10042  dfac5lem4OLD  10044  kmlem9  10075  sornom  10193  zorn2lem6  10417  elwina  10603  elina  10604  bcn1  14269  summo  15673  prodmo  15895  vdwlem12  16957  pslem  18532  gaorb  19276  gsumval3eu  19873  ringinvnz1ne0  20275  cygznlem3  21562  mat1ov  22426  dmatmulcl  22478  scmatscmiddistr  22486  scmatscm  22491  1mavmul  22526  chmatval  22807  dscmet  24550  dscopn  24551  iundisj2  25529  ltsval2  27637  wlkres  29755  wlkp1lem8  29765  1wlkdlem4  30228  frgr2wwlk1  30417  iundisj2f  32678  iundisj2fi  32888  pfxwlk  35325  erdszelem9  35400  satfv0  35559  satfv0fun  35572  satffunlem  35602  satffunlem1lem1  35603  satffunlem2lem1  35605  fununiq  35970  bj-opelidb  37485  bj-ideqgALT  37491  bj-idreseq  37495  bj-idreseqb  37496  bj-ideqg1  37497  bj-ideqg1ALT  37498  unirep  38052  eqeqan2d  38580  disjimeceqim2  39143  eldisjim3  39153  csbfv12gALTVD  45346  fcoresf1  47532  imasetpreimafvbijlemf1  47879  prproropf1olem4  47981  paireqne  47986  prmdvdsfmtnof1lem2  48063  uspgrsprf1  48638  oppcendc  49508  discsubc  49554  euendfunc  50016  mndtcbas2  50073