Theorem xpeq12 5684

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5175  df-xp 5665

This theorem is referenced by:  xpeq12i  5687  xpeq12d  5690  xpid11  5920  xp11  6172  infxpenlem  9993  pwfseqlem4a  10642  pwfseqlem4  10643  pwfseqlem5  10644  pwfseq  10645  pwsval  17535  mamufval  22514  mvmulfval  22664  txtopon  23713  txbasval  23728  txindislem  23755  ismet  24445  isxmet  24446  shsval  31601  sat1el2xp  35766  bj-imdirvallem  37707  prdsbnd2  38329  ismgmOLD  38384  opidon2OLD  38388  ttac  43648  rfovd  44612  fsovrfovd  44620  sblpnf  44905