Theorem xpeq12 5574

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   × cxp 5547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-opab 5121  df-xp 5555

This theorem is referenced by:  xpeq12i  5577  xpeq12d  5580  xpid11  5796  xp11  6026  infxpenlem  9433  fpwwe2lem5  10050  pwfseqlem4a  10077  pwfseqlem4  10078  pwfseqlem5  10079  pwfseq  10080  pwsval  16753  mamufval  20990  mvmulfval  21145  txtopon  22193  txbasval  22208  txindislem  22235  ismet  22927  isxmet  22928  shsval  29083  sat1el2xp  32621  bj-imdirval  34466  prdsbnd2  35067  ismgmOLD  35122  opidon2OLD  35126  ttac  39626  rfovd  40340  fsovrfovd  40348  sblpnf  40635