Theorem eqeq12 2835

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 2825	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqeq2 2833	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷))
3	1, 2	sylan9bb 512	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  eqeq12d  2837  eqeqan12dALT  2839  funopg  6389  eqfnfv  6802  2f1fvneq  7018  riotaeqimp  7140  soxp  7823  tfr3  8035  xpdom2  8612  dfac5lem4  9552  kmlem9  9584  sornom  9699  zorn2lem6  9923  elwina  10108  elina  10109  bcn1  13674  summo  15074  prodmo  15290  vdwlem12  16328  pslem  17816  gaorb  18437  gsumval3eu  19024  ringinvnz1ne0  19342  cygznlem3  20716  mat1ov  21057  dmatmulcl  21109  scmatscmiddistr  21117  scmatscm  21122  1mavmul  21157  chmatval  21437  dscmet  23182  dscopn  23183  iundisj2  24150  wlkres  27452  wlkp1lem8  27462  1wlkdlem4  27919  frgr2wwlk1  28108  iundisj2f  30340  iundisj2fi  30520  pfxwlk  32370  erdszelem9  32446  satfv0  32605  satfv0fun  32618  satffunlem  32648  satffunlem1lem1  32649  satffunlem2lem1  32651  fununiq  33012  sltval2  33163  bj-opelidb  34447  bj-ideqgALT  34453  bj-idreseq  34457  bj-idreseqb  34458  bj-ideqg1  34459  bj-ideqg1ALT  34460  unirep  35003  eqeqan2d  35518  csbfv12gALTVD  41253  imasetpreimafvbijlemf1  43584  prproropf1olem4  43688  paireqne  43693  prmdvdsfmtnof1lem2  43767  uspgrsprf1  44042