Theorem xpeq12 5338

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

Syntax hints:   → wi 4   ∧ wa 385   = wceq 1653   × cxp 5311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2778

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-opab 4907  df-xp 5319

This theorem is referenced by:  xpeq12i  5341  xpeq12d  5344  xpid11  5551  xp11  5787  infxpenlem  9123  fpwwe2lem5  9745  pwfseqlem4a  9772  pwfseqlem4  9773  pwfseqlem5  9774  pwfseq  9775  pwsval  16460  mamufval  20515  mvmulfval  20673  txtopon  21722  txbasval  21737  txindislem  21764  ismet  22455  isxmet  22456  shsval  28695  prdsbnd2  34080  ismgmOLD  34135  opidon2OLD  34139  ttac  38383  rfovd  39072  fsovrfovd  39080  sblpnf  39286