Theorem xpeq12 5687

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   × cxp 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5178  df-xp 5668

This theorem is referenced by:  xpeq12i  5690  xpeq12d  5693  xpid11  5923  xp11  6174  infxpenlem  9996  pwfseqlem4a  10645  pwfseqlem4  10646  pwfseqlem5  10647  pwfseq  10648  pwsval  17538  mamufval  22517  mvmulfval  22667  txtopon  23716  txbasval  23731  txindislem  23758  ismet  24448  isxmet  24449  shsval  31604  sat1el2xp  35769  bj-imdirvallem  37711  prdsbnd2  38333  ismgmOLD  38388  opidon2OLD  38392  ttac  43654  rfovd  44618  fsovrfovd  44626  sblpnf  44911