Theorem xpeq12 5657

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

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

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 5163  df-xp 5638

This theorem is referenced by:  xpeq12i  5660  xpeq12d  5663  xpid11  5889  xp11  6141  infxpenlem  9935  pwfseqlem4a  10584  pwfseqlem4  10585  pwfseqlem5  10586  pwfseq  10587  pwsval  17418  mamufval  22348  mvmulfval  22498  txtopon  23547  txbasval  23562  txindislem  23589  ismet  24279  isxmet  24280  shsval  31400  sat1el2xp  35595  bj-imdirvallem  37435  prdsbnd2  38046  ismgmOLD  38101  opidon2OLD  38105  ttac  43393  rfovd  44357  fsovrfovd  44365  sblpnf  44666