Theorem xpeq12 5643

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   × cxp 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-opab 5135  df-xp 5624

This theorem is referenced by:  xpeq12i  5646  xpeq12d  5649  xpid11  5874  xp11  6126  infxpenlem  9926  pwfseqlem4a  10575  pwfseqlem4  10576  pwfseqlem5  10577  pwfseq  10578  pwsval  17440  mamufval  22375  mvmulfval  22525  txtopon  23574  txbasval  23589  txindislem  23616  ismet  24306  isxmet  24307  shsval  31401  sat1el2xp  35607  bj-imdirvallem  37540  prdsbnd2  38162  ismgmOLD  38217  opidon2OLD  38221  ttac  43481  rfovd  44445  fsovrfovd  44453  sblpnf  44754