Theorem xpeq12 5725

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-xp 5706

This theorem is referenced by:  xpeq12i  5728  xpeq12d  5731  xpid11  5957  xp11  6206  infxpenlem  10082  pwfseqlem4a  10730  pwfseqlem4  10731  pwfseqlem5  10732  pwfseq  10733  pwsval  17546  mamufval  22417  mvmulfval  22569  txtopon  23620  txbasval  23635  txindislem  23662  ismet  24354  isxmet  24355  shsval  31344  sat1el2xp  35347  bj-imdirvallem  37146  prdsbnd2  37755  ismgmOLD  37810  opidon2OLD  37814  ttac  42993  rfovd  43963  fsovrfovd  43971  sblpnf  44279