Theorem xpeq12 5605

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-xp 5586

This theorem is referenced by:  xpeq12i  5608  xpeq12d  5611  xpid11  5830  xp11  6067  infxpenlem  9700  fpwwe2lem4  10321  pwfseqlem4a  10348  pwfseqlem4  10349  pwfseqlem5  10350  pwfseq  10351  pwsval  17114  mamufval  21444  mvmulfval  21599  txtopon  22650  txbasval  22665  txindislem  22692  ismet  23384  isxmet  23385  shsval  29575  sat1el2xp  33241  bj-imdirvallem  35278  prdsbnd2  35880  ismgmOLD  35935  opidon2OLD  35939  ttac  40774  rfovd  41498  fsovrfovd  41506  sblpnf  41817