Theorem xpeq12 5684

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-opab 5187  df-xp 5665

This theorem is referenced by:  xpeq12i  5687  xpeq12d  5690  xpid11  5917  xp11  6169  infxpenlem  10032  pwfseqlem4a  10680  pwfseqlem4  10681  pwfseqlem5  10682  pwfseq  10683  pwsval  17505  mamufval  22335  mvmulfval  22485  txtopon  23534  txbasval  23549  txindislem  23576  ismet  24267  isxmet  24268  shsval  31298  sat1el2xp  35406  bj-imdirvallem  37203  prdsbnd2  37824  ismgmOLD  37879  opidon2OLD  37883  ttac  43027  rfovd  43992  fsovrfovd  44000  sblpnf  44301