Theorem xpeq12 5615

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-opab 5138  df-xp 5596

This theorem is referenced by:  xpeq12i  5618  xpeq12d  5621  xpid11  5844  xp11  6083  infxpenlem  9778  fpwwe2lem4  10399  pwfseqlem4a  10426  pwfseqlem4  10427  pwfseqlem5  10428  pwfseq  10429  pwsval  17206  mamufval  21543  mvmulfval  21700  txtopon  22751  txbasval  22766  txindislem  22793  ismet  23485  isxmet  23486  shsval  29683  sat1el2xp  33350  bj-imdirvallem  35360  prdsbnd2  35962  ismgmOLD  36017  opidon2OLD  36021  ttac  40865  rfovd  41616  fsovrfovd  41624  sblpnf  41935