Theorem xpeq12 5688

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-xp 5669

This theorem is used by:  xpeq12i  5691  xpeq12d  5694  xpid11  5924  xp11  6175  infxpenlem  10013  pwfseqlem4a  10661  pwfseqlem4  10662  pwfseqlem5  10663  pwfseq  10664  pwsval  17561  mamufval  22599  mvmulfval  22749  txtopon  23799  txbasval  23814  txindislem  23841  ismet  24531  isxmet  24532  shsval  31735  sat1el2xp  35908  bj-imdirvallem  37881  prdsbnd2  38504  ismgmOLD  38559  opidon2OLD  38563  ttac  43821  rfovd  44785  fsovrfovd  44793  sblpnf  45078