Theorem xpeq12 5666

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-xp 5647

This theorem is referenced by:  xpeq12i  5669  xpeq12d  5672  xpid11  5899  xp11  6151  infxpenlem  9973  pwfseqlem4a  10621  pwfseqlem4  10622  pwfseqlem5  10623  pwfseq  10624  pwsval  17456  mamufval  22286  mvmulfval  22436  txtopon  23485  txbasval  23500  txindislem  23527  ismet  24218  isxmet  24219  shsval  31248  sat1el2xp  35373  bj-imdirvallem  37175  prdsbnd2  37796  ismgmOLD  37851  opidon2OLD  37855  ttac  43032  rfovd  43997  fsovrfovd  44005  sblpnf  44306