Theorem eqeq12 2746

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqeqan12dALT  2748  funopg  6534  eqfnfv  6985  riotaeqimp  7352  soxp  8085  tfr3  8344  xpdom2  9013  dfac5lem4  10055  dfac5lem4OLD  10057  kmlem9  10088  sornom  10206  zorn2lem6  10430  elwina  10615  elina  10616  bcn1  14254  summo  15659  prodmo  15878  vdwlem12  16939  pslem  18507  gaorb  19215  gsumval3eu  19810  ringinvnz1ne0  20185  cygznlem3  21455  mat1ov  22311  dmatmulcl  22363  scmatscmiddistr  22371  scmatscm  22376  1mavmul  22411  chmatval  22692  dscmet  24436  dscopn  24437  iundisj2  25426  sltval2  27544  wlkres  29572  wlkp1lem8  29582  1wlkdlem4  30042  frgr2wwlk1  30231  iundisj2f  32492  iundisj2fi  32693  pfxwlk  35084  erdszelem9  35159  satfv0  35318  satfv0fun  35331  satffunlem  35361  satffunlem1lem1  35362  satffunlem2lem1  35364  fununiq  35729  bj-opelidb  37113  bj-ideqgALT  37119  bj-idreseq  37123  bj-idreseqb  37124  bj-ideqg1  37125  bj-ideqg1ALT  37126  unirep  37681  eqeqan2d  38197  csbfv12gALTVD  44861  fcoresf1  47043  imasetpreimafvbijlemf1  47378  prproropf1olem4  47480  paireqne  47485  prmdvdsfmtnof1lem2  47559  uspgrsprf1  48108  oppcendc  48980  discsubc  49026  euendfunc  49488  mndtcbas2  49545