Theorem xpeq12 5644

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

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

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 5155  df-xp 5625

This theorem is referenced by:  xpeq12i  5647  xpeq12d  5650  xpid11  5874  xp11  6124  infxpenlem  9907  pwfseqlem4a  10555  pwfseqlem4  10556  pwfseqlem5  10557  pwfseq  10558  pwsval  17390  mamufval  22277  mvmulfval  22427  txtopon  23476  txbasval  23491  txindislem  23518  ismet  24209  isxmet  24210  shsval  31256  sat1el2xp  35352  bj-imdirvallem  37154  prdsbnd2  37775  ismgmOLD  37830  opidon2OLD  37834  ttac  43009  rfovd  43974  fsovrfovd  43982  sblpnf  44283