Theorem xpeq12 5686

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   × cxp 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5174  df-xp 5667

This theorem is referenced by:  xpeq12i  5689  xpeq12d  5692  xpid11  5922  xp11  6173  infxpenlem  9993  pwfseqlem4a  10641  pwfseqlem4  10642  pwfseqlem5  10643  pwfseq  10644  pwsval  17534  mamufval  22549  mvmulfval  22699  txtopon  23748  txbasval  23763  txindislem  23790  ismet  24480  isxmet  24481  shsval  31664  sat1el2xp  35871  bj-imdirvallem  37824  prdsbnd2  38446  ismgmOLD  38501  opidon2OLD  38505  ttac  43763  rfovd  44727  fsovrfovd  44735  sblpnf  45020