Theorem xpeq12 5672

Description: Equality theorem for Cartesian product. (Contributed by FL, 31-Aug-2009.)

Assertion

Ref	Expression
xpeq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Proof of Theorem xpeq12

Step	Hyp	Ref	Expression
1		xpeq1 5661	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
2		xpeq2 5668	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷))
3	1, 2	sylan9eq 2817	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   × cxp 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-opab 5163  df-xp 5653

This theorem is referenced by:  xpeq12i  5675  xpeq12d  5678  xpid11  5908  xp11  6161  infxpenlem  9969  pwfseqlem4a  10619  pwfseqlem4  10620  pwfseqlem5  10621  pwfseq  10622  pwsval  17515  mamufval  22449  mvmulfval  22599  txtopon  23648  txbasval  23663  txindislem  23690  ismet  24380  isxmet  24381  shsval  31512  sat1el2xp  35726  bj-imdirvallem  37669  prdsbnd2  38291  ismgmOLD  38346  opidon2OLD  38350  ttac  43610  rfovd  44574  fsovrfovd  44582  sblpnf  44883