Theorem xpeq12 5656

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   × cxp 5629

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-xp 5637

This theorem is referenced by:  xpeq12i  5659  xpeq12d  5662  xpid11  5887  xp11  6139  infxpenlem  9935  pwfseqlem4a  10584  pwfseqlem4  10585  pwfseqlem5  10586  pwfseq  10587  pwsval  17449  mamufval  22357  mvmulfval  22507  txtopon  23556  txbasval  23571  txindislem  23598  ismet  24288  isxmet  24289  shsval  31383  sat1el2xp  35561  bj-imdirvallem  37494  prdsbnd2  38116  ismgmOLD  38171  opidon2OLD  38175  ttac  43464  rfovd  44428  fsovrfovd  44436  sblpnf  44737