Theorem xpeq12d 5293

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 5287	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 × 𝐶) = (𝐵 × 𝐷))
4	1, 2, 3	syl2anc 696	1 ⊢ (𝜑 → (𝐴 × 𝐶) = (𝐵 × 𝐷))

Syntax hints:   → wi 4   = wceq 1628   × cxp 5260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-opab 4861  df-xp 5268

This theorem is referenced by:  sqxpeqd  5294  opeliunxp  5323  mpt2mptsx  7397  dmmpt2ssx  7399  fmpt2x  7400  ovmptss  7422  fparlem3  7443  fparlem4  7444  erssxp  7930  marypha2lem2  8503  ackbij1lem8  9237  r1om  9254  fictb  9255  axcc2lem  9446  axcc2  9447  axdc4lem  9465  fsum2dlem  14696  fsumcom2  14700  fsumcom2OLD  14701  ackbijnn  14755  fprod2dlem  14905  fprodcom2  14909  fprodcom2OLD  14910  homaval  16878  xpcval  17014  xpchom  17017  xpchom2  17023  1stfval  17028  2ndfval  17031  xpcpropd  17045  evlfval  17054  isga  17920  symgval  17995  gsumcom2  18570  gsumxp  18571  ablfaclem3  18682  psrval  19560  mamufval  20389  mamudm  20392  mvmulfval  20546  mavmuldm  20554  mavmul0g  20557  txbas  21568  ptbasfi  21582  txindis  21635  tmsxps  22538  metustexhalf  22558  aciunf1lem  29767  esum2dlem  30459  cvmliftlem15  31583  mexval  31702  mpstval  31735  mclsval  31763  mclsax  31769  mclsppslem  31783  filnetlem4  32678  poimirlem26  33744  poimirlem28  33746  heiborlem3  33921  elrefrels2  34586  refreleq  34589  elcnvrefrels2  34599  dvhfset  36867  dvhset  36868  dibffval  36927  dibfval  36928  hdmap1fval  37584  opeliun2xp  42617  dmmpt2ssx2  42621