Theorem xpeq12 5663

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5173  df-xp 5644

This theorem is referenced by:  xpeq12i  5666  xpeq12d  5669  xpid11  5892  xp11  6132  infxpenlem  9958  fpwwe2lem4  10579  pwfseqlem4a  10606  pwfseqlem4  10607  pwfseqlem5  10608  pwfseq  10609  pwsval  17382  mamufval  21771  mvmulfval  21928  txtopon  22979  txbasval  22994  txindislem  23021  ismet  23713  isxmet  23714  shsval  30317  sat1el2xp  34060  bj-imdirvallem  35724  prdsbnd2  36327  ismgmOLD  36382  opidon2OLD  36386  ttac  41418  rfovd  42395  fsovrfovd  42403  sblpnf  42712