Theorem eqeq12 2819

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

Assertion

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

Proof of Theorem eqeq12

Step	Hyp	Ref	Expression
1		eqeq1 2810	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqeq2 2817	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷))
3	1, 2	sylan9bb 501	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799

This theorem is referenced by:  eqeq12d  2821  eqeqan12dALT  2823  funopg  6135  eqfnfv  6533  2f1fvneq  6741  riotaeqimp  6858  soxp  7524  tfr3  7731  xpdom2  8294  dfac5lem4  9232  kmlem9  9265  sornom  9384  zorn2lem6  9608  elwina  9793  elina  9794  bcn1  13320  summo  14671  prodmo  14887  vdwlem12  15913  pslem  17411  gaorb  17941  gsumval3eu  18506  ringinvnz1ne0  18794  cygznlem3  20125  mat1ov  20465  dmatmulcl  20517  scmatscmiddistr  20525  scmatscm  20530  1mavmul  20565  chmatval  20847  dscmet  22590  dscopn  22591  iundisj2  23530  wlkres  26795  wlkp1lem8  26805  1wlkdlem4  27313  frgr2wwlk1  27504  iundisj2f  29728  iundisj2fi  29883  erdszelem9  31504  fununiq  31989  sltval2  32130  bj-elid  33401  unirep  33819  eqeqan1d  34324  eqeqan2d  34325  csbfv12gALTVD  39629  prmdvdsfmtnof1lem2  42072  uspgrsprf1  42323