Theorem xpeq12d 5354

Description: Equality deduction for Cartesian product. (Contributed by NM, 8-Dec-2013.)

Hypotheses

Ref	Expression
xpeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
xpeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
xpeq12d	⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Proof of Theorem xpeq12d

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		xpeq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		xpeq12 5348	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
4	1, 2, 3	syl2anc 575	1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Syntax hints:   → wi 4   = wceq 1637   × cxp 5322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-opab 4918  df-xp 5330

This theorem is referenced by:  sqxpeqd  5355  opeliunxp  5384  mpt2mptsx  7476  dmmpt2ssx  7478  fmpt2x  7479  ovmptss  7502  fparlem3  7523  fparlem4  7524  erssxp  8012  marypha2lem2  8591  ackbij1lem8  9344  r1om  9361  fictb  9362  axcc2lem  9553  axcc2  9554  axdc4lem  9572  fsum2dlem  14744  fsumcom2  14748  ackbijnn  14802  fprod2dlem  14951  fprodcom2  14955  homaval  16905  xpcval  17042  xpchom  17045  xpchom2  17051  1stfval  17056  2ndfval  17059  xpcpropd  17073  evlfval  17082  isga  17945  symgval  18020  gsumcom2  18595  gsumxp  18596  ablfaclem3  18708  psrval  19591  mamufval  20422  mamudm  20425  mvmulfval  20580  mavmuldm  20588  mavmul0g  20591  txbas  21605  ptbasfi  21619  txindis  21672  tmsxps  22575  metustexhalf  22595  aciunf1lem  29812  esum2dlem  30502  cvmliftlem15  31625  mexval  31744  mpstval  31777  mclsval  31805  mclsax  31811  mclsppslem  31825  filnetlem4  32719  poimirlem26  33767  poimirlem28  33769  heiborlem3  33942  elrefrels2  34599  refreleq  34602  elcnvrefrels2  34612  dvhfset  36879  dvhset  36880  dibffval  36939  dibfval  36940  hdmap1fval  37595  opeliun2xp  42697  dmmpt2ssx2  42701