Theorem xpeq12 5650

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-xp 5631

This theorem is referenced by:  xpeq12i  5653  xpeq12d  5656  xpid11  5882  xp11  6134  infxpenlem  9929  pwfseqlem4a  10578  pwfseqlem4  10579  pwfseqlem5  10580  pwfseq  10581  pwsval  17443  mamufval  22370  mvmulfval  22520  txtopon  23569  txbasval  23584  txindislem  23611  ismet  24301  isxmet  24302  shsval  31401  sat1el2xp  35580  bj-imdirvallem  37513  prdsbnd2  38133  ismgmOLD  38188  opidon2OLD  38192  ttac  43485  rfovd  44449  fsovrfovd  44457  sblpnf  44758