Theorem eqeq12 2779

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  eqeqan12dALT  2781  funopg  6555  eqfnfv  7011  riotaeqimp  7379  soxp  8109  tfr3  8370  xpdom2  9044  dfac5lem4  10082  dfac5lem4OLD  10084  kmlem9  10115  sornom  10234  zorn2lem6  10458  elwina  10644  elina  10645  bcn1  14326  summo  15744  prodmo  15966  vdwlem12  17028  pslem  18604  gaorb  19347  gsumval3eu  19944  ringinvnz1ne0  20346  cygznlem3  21618  mat1ov  22505  dmatmulcl  22557  scmatscmiddistr  22565  scmatscm  22570  1mavmul  22605  chmatval  22886  dscmet  24629  dscopn  24630  iundisj2  25608  ltsval2  27717  brprlng  29062  wlkres  29866  wlkp1lem8  29876  1wlkdlem4  30339  frgr2wwlk1  30528  iundisj2f  32787  iundisj2fi  32996  pfxwlk  35471  erdszelem9  35546  satfv0  35705  satfv0fun  35718  satffunlem  35748  satffunlem1lem1  35749  satffunlem2lem1  35751  fununiq  36116  bj-opelidb  37641  bj-ideqgALT  37647  bj-idreseq  37651  bj-idreseqb  37652  bj-ideqg1  37653  bj-ideqg1ALT  37654  unirep  38210  eqeqan2d  38738  disjimeceqim2  39301  eldisjim3  39311  csbfv12gALTVD  45471  fcoresf1  47660  imasetpreimafvbijlemf1  48007  prproropf1olem4  48109  paireqne  48114  prmdvdsfmtnof1lem2  48191  uspgrsprf1  48766  oppcendc  49636  discsubc  49682  euendfunc  50144  mndtcbas2  50201