Theorem eqeq12 2782

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  eqeqan12dALT  2784  funopg  6574  eqfnfv  7029  riotaeqimp  7402  soxp  8131  tfr3  8392  xpdom2  9067  dfac5lem4  10126  kmlem9  10158  sornom  10276  zorn2lem6  10500  elwina  10686  elina  10687  bcn1  14367  summo  15791  prodmo  16013  vdwlem12  17074  pslem  18650  gaorb  19421  gsumval3eu  20018  ringinvnz1ne0  20429  cygznlem3  21769  mat1ov  22655  dmatmulcl  22707  scmatscmiddistr  22715  scmatscm  22720  1mavmul  22755  chmatval  23036  dscmet  24780  dscopn  24781  iundisj2  25759  ltsval2  27871  brprlng  29243  wlkres  30076  wlkp1lem8  30086  pfxwlk  30093  1wlkdlem4  30558  frgr2wwlk1  30751  iundisj2f  33006  iundisj2fi  33212  erdszelem9  35728  satfv0  35887  satfv0fun  35900  satffunlem  35930  satffunlem1lem1  35931  satffunlem2lem1  35933  fununiq  36298  bj-opelidb  37853  bj-ideqgALT  37859  bj-idreseq  37863  bj-idreseqb  37864  bj-ideqg1  37865  bj-ideqg1ALT  37866  unirep  38423  eqeqan2d  38949  disjimeceqim2  39512  eldisjim3  39522  csbfv12gALTVD  45665  fcoresf1  47864  imasetpreimafvbijlemf1  48211  prproropf1olem4  48313  paireqne  48318  prmdvdsfmtnof1lem2  48395  uspgrsprf1  48970  oppcendc  49853  discsubc  49899  euendfunc  50361  mndtcbas2  50418