Theorem eqeq12 2833

Description: Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
eqeq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Proof of Theorem eqeq12

Step	Hyp	Ref	Expression
1		eqeq1 2823	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqeq2 2831	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷))
3	1, 2	sylan9bb 512	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812

This theorem is referenced by:  eqeq12d  2835  eqeqan12dALT  2837  funopg  6382  eqfnfv  6795  2f1fvneq  7010  riotaeqimp  7132  soxp  7815  tfr3  8027  xpdom2  8604  dfac5lem4  9544  kmlem9  9576  sornom  9691  zorn2lem6  9915  elwina  10100  elina  10101  bcn1  13665  summo  15066  prodmo  15282  vdwlem12  16320  pslem  17808  gaorb  18429  gsumval3eu  19016  ringinvnz1ne0  19334  cygznlem3  20708  mat1ov  21049  dmatmulcl  21101  scmatscmiddistr  21109  scmatscm  21114  1mavmul  21149  chmatval  21429  dscmet  23174  dscopn  23175  iundisj2  24142  wlkres  27444  wlkp1lem8  27454  1wlkdlem4  27911  frgr2wwlk1  28100  iundisj2f  30332  iundisj2fi  30512  pfxwlk  32363  erdszelem9  32439  satfv0  32598  satfv0fun  32611  satffunlem  32641  satffunlem1lem1  32642  satffunlem2lem1  32644  fununiq  33005  sltval2  33156  bj-opelidb  34436  bj-ideqgALT  34442  bj-idreseq  34446  bj-idreseqb  34447  bj-ideqg1  34448  bj-ideqg1ALT  34449  unirep  34980  eqeqan2d  35495  csbfv12gALTVD  41224  imasetpreimafvbijlemf1  43555  prproropf1olem4  43659  paireqne  43664  prmdvdsfmtnof1lem2  43738  uspgrsprf1  44013