Theorem xpeq12 5665

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   × cxp 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5172  df-xp 5646

This theorem is referenced by:  xpeq12i  5668  xpeq12d  5671  xpid11  5898  xp11  6150  infxpenlem  9972  pwfseqlem4a  10620  pwfseqlem4  10621  pwfseqlem5  10622  pwfseq  10623  pwsval  17455  mamufval  22285  mvmulfval  22435  txtopon  23484  txbasval  23499  txindislem  23526  ismet  24217  isxmet  24218  shsval  31247  sat1el2xp  35366  bj-imdirvallem  37163  prdsbnd2  37784  ismgmOLD  37839  opidon2OLD  37843  ttac  43018  rfovd  43983  fsovrfovd  43991  sblpnf  44292