Theorem xpeq12 5680

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-xp 5661

This theorem is used by:  xpeq12i  5683  xpeq12d  5686  xpid11  5916  xp11  6168  infxpenlem  10016  pwfseqlem4a  10670  pwfseqlem4  10671  pwfseqlem5  10672  pwfseq  10673  pwsval  17571  mamufval  22614  mvmulfval  22764  txtopon  23817  txbasval  23832  txindislem  23859  ismet  24549  isxmet  24550  shsval  31793  sat1el2xp  35958  bj-imdirvallem  37932  prdsbnd2  38545  ismgmOLD  38600  opidon2OLD  38604  ttac  43877  rfovd  44841  fsovrfovd  44849  sblpnf  45134