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 2815	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-xp 5657

This theorem is used by:  xpeq12i  5679  xpeq12d  5682  xpid11  5915  xp11  6169  infxpenlem  10099  pwfseqlem4a  10753  pwfseqlem4  10754  pwfseqlem5  10755  pwfseq  10756  pwsval  17666  mamufval  22716  mvmulfval  22866  txtopon  23919  txbasval  23934  txindislem  23961  ismet  24651  isxmet  24652  shsval  31923  sat1el2xp  36234  bj-imdirvallem  38210  prdsbnd2  38838  ismgmOLD  38893  opidon2OLD  38897  ttac  44152  rfovd  45110  fsovrfovd  45118  sblpnf  45403