Theorem xpeq12 5683

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5174  df-xp 5664

This theorem is used by:  xpeq12i  5686  xpeq12d  5689  xpid11  5926  xp11  6185  infxpenlem  10131  pwfseqlem4a  10785  pwfseqlem4  10786  pwfseqlem5  10787  pwfseq  10788  pwsval  17707  mamufval  22762  mvmulfval  22912  txtopon  23965  txbasval  23980  txindislem  24007  ismet  24697  isxmet  24698  shsval  31971  sat1el2xp  36352  bj-imdirvallem  38369  prdsbnd2  38995  ismgmOLD  39050  opidon2OLD  39054  ttac  44309  rfovd  45262  fsovrfovd  45270  sblpnf  45555