Theorem xpeq12 5663

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

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

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 5170  df-xp 5644

This theorem is referenced by:  xpeq12i  5666  xpeq12d  5669  xpid11  5896  xp11  6148  infxpenlem  9966  pwfseqlem4a  10614  pwfseqlem4  10615  pwfseqlem5  10616  pwfseq  10617  pwsval  17449  mamufval  22279  mvmulfval  22429  txtopon  23478  txbasval  23493  txindislem  23520  ismet  24211  isxmet  24212  shsval  31241  sat1el2xp  35366  bj-imdirvallem  37168  prdsbnd2  37789  ismgmOLD  37844  opidon2OLD  37848  ttac  43025  rfovd  43990  fsovrfovd  43998  sblpnf  44299