Theorem xpeq12 5676

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  xpeq12i  5679  xpeq12d  5682  xpid11  5914  xp11  6167  infxpenlem  10085  pwfseqlem4a  10739  pwfseqlem4  10740  pwfseqlem5  10741  pwfseq  10742  pwsval  17650  mamufval  22700  mvmulfval  22850  txtopon  23903  txbasval  23918  txindislem  23945  ismet  24635  isxmet  24636  shsval  31907  sat1el2xp  36123  bj-imdirvallem  38081  prdsbnd2  38709  ismgmOLD  38764  opidon2OLD  38768  ttac  44022  rfovd  44986  fsovrfovd  44994  sblpnf  45279