Theorem xpeq12 5656

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5165  df-xp 5637

This theorem is referenced by:  xpeq12i  5659  xpeq12d  5662  xpid11  5885  xp11  6136  infxpenlem  9942  pwfseqlem4a  10590  pwfseqlem4  10591  pwfseqlem5  10592  pwfseq  10593  pwsval  17425  mamufval  22255  mvmulfval  22405  txtopon  23454  txbasval  23469  txindislem  23496  ismet  24187  isxmet  24188  shsval  31214  sat1el2xp  35339  bj-imdirvallem  37141  prdsbnd2  37762  ismgmOLD  37817  opidon2OLD  37821  ttac  42998  rfovd  43963  fsovrfovd  43971  sblpnf  44272