Theorem xpeq12 5647

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 5636	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
2		xpeq2 5643	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 × 𝐶) = (𝐵 × 𝐷))
3	1, 2	sylan9eq 2789	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   × cxp 5620

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-opab 5159  df-xp 5628

This theorem is referenced by:  xpeq12i  5650  xpeq12d  5653  xpid11  5879  xp11  6131  infxpenlem  9921  pwfseqlem4a  10570  pwfseqlem4  10571  pwfseqlem5  10572  pwfseq  10573  pwsval  17404  mamufval  22334  mvmulfval  22484  txtopon  23533  txbasval  23548  txindislem  23575  ismet  24265  isxmet  24266  shsval  31336  sat1el2xp  35522  bj-imdirvallem  37324  prdsbnd2  37935  ismgmOLD  37990  opidon2OLD  37994  ttac  43220  rfovd  44184  fsovrfovd  44192  sblpnf  44493