Theorem xpeq12 5649

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-xp 5630

This theorem is referenced by:  xpeq12i  5652  xpeq12d  5655  xpid11  5881  xp11  6133  infxpenlem  9923  pwfseqlem4a  10572  pwfseqlem4  10573  pwfseqlem5  10574  pwfseq  10575  pwsval  17406  mamufval  22336  mvmulfval  22486  txtopon  23535  txbasval  23550  txindislem  23577  ismet  24267  isxmet  24268  shsval  31387  sat1el2xp  35573  bj-imdirvallem  37385  prdsbnd2  37996  ismgmOLD  38051  opidon2OLD  38055  ttac  43278  rfovd  44242  fsovrfovd  44250  sblpnf  44551