Theorem eqeq12 2750

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  eqeq12d  2752  eqeqan12dALT  2754  funopg  6392  eqfnfv  6830  2f1fvneq  7050  riotaeqimp  7175  soxp  7874  tfr3  8113  xpdom2  8718  dfac5lem4  9705  kmlem9  9737  sornom  9856  zorn2lem6  10080  elwina  10265  elina  10266  bcn1  13844  summo  15246  prodmo  15461  vdwlem12  16508  pslem  18032  gaorb  18655  gsumval3eu  19243  ringinvnz1ne0  19564  cygznlem3  20488  mat1ov  21299  dmatmulcl  21351  scmatscmiddistr  21359  scmatscm  21364  1mavmul  21399  chmatval  21680  dscmet  23424  dscopn  23425  iundisj2  24400  wlkres  27712  wlkp1lem8  27722  1wlkdlem4  28177  frgr2wwlk1  28366  iundisj2f  30602  iundisj2fi  30792  pfxwlk  32752  erdszelem9  32828  satfv0  32987  satfv0fun  33000  satffunlem  33030  satffunlem1lem1  33031  satffunlem2lem1  33033  fununiq  33413  sltval2  33545  bj-opelidb  35007  bj-ideqgALT  35013  bj-idreseq  35017  bj-idreseqb  35018  bj-ideqg1  35019  bj-ideqg1ALT  35020  unirep  35557  eqeqan2d  36069  csbfv12gALTVD  42133  fcoresf1  44178  imasetpreimafvbijlemf1  44472  prproropf1olem4  44574  paireqne  44579  prmdvdsfmtnof1lem2  44653  uspgrsprf1  44925  mndtcbas2  45984