Theorem eqeq12 2752

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 2749	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 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  eqeqan12dALT  2757  funopg  6602  eqfnfv  7051  2f1fvneq  7280  riotaeqimp  7414  soxp  8153  tfr3  8438  xpdom2  9106  dfac5lem4  10164  dfac5lem4OLD  10166  kmlem9  10197  sornom  10315  zorn2lem6  10539  elwina  10724  elina  10725  bcn1  14349  summo  15750  prodmo  15969  vdwlem12  17026  pslem  18630  gaorb  19338  gsumval3eu  19937  ringinvnz1ne0  20314  cygznlem3  21606  mat1ov  22470  dmatmulcl  22522  scmatscmiddistr  22530  scmatscm  22535  1mavmul  22570  chmatval  22851  dscmet  24601  dscopn  24602  iundisj2  25598  sltval2  27716  wlkres  29703  wlkp1lem8  29713  1wlkdlem4  30169  frgr2wwlk1  30358  iundisj2f  32610  iundisj2fi  32805  pfxwlk  35108  erdszelem9  35184  satfv0  35343  satfv0fun  35356  satffunlem  35386  satffunlem1lem1  35387  satffunlem2lem1  35389  fununiq  35750  bj-opelidb  37135  bj-ideqgALT  37141  bj-idreseq  37145  bj-idreseqb  37146  bj-ideqg1  37147  bj-ideqg1ALT  37148  unirep  37701  eqeqan2d  38217  csbfv12gALTVD  44897  fcoresf1  47019  imasetpreimafvbijlemf1  47329  prproropf1olem4  47431  paireqne  47436  prmdvdsfmtnof1lem2  47510  uspgrsprf1  47991  mndtcbas2  48892