Theorem xpeq12 5709

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   × cxp 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-opab 5205  df-xp 5690

This theorem is referenced by:  xpeq12i  5712  xpeq12d  5715  xpid11  5942  xp11  6194  infxpenlem  10054  pwfseqlem4a  10702  pwfseqlem4  10703  pwfseqlem5  10704  pwfseq  10705  pwsval  17532  mamufval  22397  mvmulfval  22549  txtopon  23600  txbasval  23615  txindislem  23642  ismet  24334  isxmet  24335  shsval  31332  sat1el2xp  35385  bj-imdirvallem  37182  prdsbnd2  37803  ismgmOLD  37858  opidon2OLD  37862  ttac  43053  rfovd  44019  fsovrfovd  44027  sblpnf  44334