Theorem eqeq12 2635

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqeq12d  2637  eqeqan12dALT  2639  funopg  5922  eqfnfv  6311  2f1fvneq  6517  riotaeqimp  6634  soxp  7290  tfr3  7495  xpdom2  8055  dfac5lem4  8949  kmlem9  8980  sornom  9099  zorn2lem6  9323  elwina  9508  elina  9509  bcn1  13100  summo  14448  prodmo  14666  vdwlem12  15696  pslem  17206  gaorb  17740  gsumval3eu  18305  ringinvnz1ne0  18592  cygznlem3  19918  mat1ov  20254  dmatmulcl  20306  scmatscmiddistr  20314  scmatscm  20319  1mavmul  20354  chmatval  20634  dscmet  22377  dscopn  22378  iundisj2  23317  wlkres  26567  wlkp1lem8  26577  1wlkdlem4  27000  frgr2wwlk1  27193  iundisj2f  29403  iundisj2fi  29556  erdszelem9  31181  fununiq  31667  sltval2  31809  bj-elid  33085  unirep  33507  eqeqan1d  34003  eqeqan2d  34004  csbfv12gALTVD  39135  prmdvdsfmtnof1lem2  41497  uspgrsprf1  41755