Theorem xpeq12 5544

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-opab 5093  df-xp 5525

This theorem is referenced by:  xpeq12i  5547  xpeq12d  5550  xpid11  5766  xp11  5999  infxpenlem  9424  fpwwe2lem5  10045  pwfseqlem4a  10072  pwfseqlem4  10073  pwfseqlem5  10074  pwfseq  10075  pwsval  16751  mamufval  20992  mvmulfval  21147  txtopon  22196  txbasval  22211  txindislem  22238  ismet  22930  isxmet  22931  shsval  29095  sat1el2xp  32739  bj-imdirvallem  34595  prdsbnd2  35233  ismgmOLD  35288  opidon2OLD  35292  ttac  39977  rfovd  40702  fsovrfovd  40710  sblpnf  41014