Theorem xpeq12d 5697

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   × cxp 5664

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-opab 5179  df-xp 5672

This theorem is used by:  sqxpeqd  5698  opeliunxp  5733  opeliun2xp  5734  mpomptsx  8070  dmmpossx  8072  fmpox  8073  ovmptss  8097  fparlem3  8118  fparlem4  8119  on2recsov  8663  naddcllem  8671  erssxp  8727  marypha2lem2  9406  ackbij1lem8  10228  r1om  10245  fictb  10246  axcc2lem  10438  axcc2  10439  axdc4lem  10457  fsum2dlem  15847  fsumcom2  15851  ackbijnn  15908  fprod2dlem  16060  fprodcom2  16064  homaval  18113  xpcval  18258  xpchom  18261  xpchom2  18267  1stfval  18272  2ndfval  18275  xpcpropd  18289  evlfval  18298  efmnd  18960  isga  19392  gsumcom2  20076  gsumxp  20077  ablfaclem3  20190  psrval  22102  mamufval  22586  mamudm  22589  mvmulfval  22736  mavmuldm  22744  mavmul0g  22747  txbas  23761  ptbasfi  23775  txindis  23828  tmsxps  24730  metustexhalf  24750  noxpordpred  28183  aciunf1lem  33044  gsumpart  33414  gsumwrd2dccatlem  33428  gsumwrd2dccat  33429  erlval  33609  rlocval  33610  fedgmullem1  34050  fldextrspunlsplem  34094  esum2dlem  34513  lpadval  35098  cvmliftlem15  35811  mexval  36015  mpstval  36048  mclsval  36076  mclsax  36082  mclsppslem  36096  filnetlem4  36933  poimirlem26  38338  poimirlem28  38340  heiborlem3  38505  cnvref4  39040  elrefrels2  39288  refreleq  39291  elcnvrefrels2  39304  dvhfset  41895  dvhset  41896  dibffval  41955  dibfval  41956  hdmap1fval  42611  dmmpossx2  49158  dmrnxp  49656  imasubclem3  49925  imaf1hom  49927  swapf2f1oaALT  50097  fucofvalg  50137  fucofvalne  50144  fucof21  50166  functhinclem1  50263  functhinclem3  50265  functhinclem4  50266