Theorem breqd 4450

Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)

Hypothesis

Ref	Expression
breq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
breqd	|- ( ph -> ( C A D <-> C B D ) )

Proof of Theorem breqd

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- ( ph -> A = B )
2		breq 4441	. 2 |- ( A = B -> ( C A D <-> C B D ) )
3	1, 2	syl 16	1 |- ( ph -> ( C A D <-> C B D ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1398   class class class wbr 4439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-cleq 2446  df-clel 2449  df-br 4440

This theorem is referenced by:  breq123d  4453  sbcbr123  4490  sbcbr  4491  sbcbr12g  4492  bropopvvv  6853  sprmpt2d  6944  supeq123d  7901  fpwwe2lem12  9008  fpwwe2  9010  brtrclfv  12920  trclfvcotr  12927  dfrtrclrec2  12972  rtrclreclem3  12975  relexpindlem  12978  shftfib  12987  2shfti  12995  prdsval  14944  pwsle  14981  pwsleval  14982  imasleval  15030  issect  15241  isinv  15248  episect  15273  brcic  15286  ciclcl  15290  cicrcl  15291  isfunc  15352  funcres2c  15389  isfull  15398  isfth  15402  fullpropd  15408  fthpropd  15409  elhoma  15510  isposd  15784  pltval  15789  lubfval  15807  glbfval  15820  joinfval  15830  meetfval  15844  odumeet  15969  odujoin  15971  ipole  15987  eqgval  16449  unitpropd  17541  ltbval  18331  opsrval  18334  znleval  18766  lmbr  19926  metustexhalfOLD  21232  metustexhalf  21233  metucnOLD  21257  metucn  21258  isphtpc  21660  dvef  22547  taylthlem1  22934  ulmval  22941  iscgrg  24105  legov  24173  ishlg  24187  opphllem5  24324  opphllem6  24325  hpgbr  24330  iscgra  24370  wlkon  24735  iswlkon  24736  wlkonprop  24737  trls  24740  trlon  24744  istrlon  24745  trlonprop  24746  pths  24770  spths  24771  pthon  24779  ispthon  24780  pthonprop  24781  spthon  24786  isspthon  24787  spthonprp  24789  cyclispthon  24835  dfconngra1  24873  isconngra  24874  isconngra1  24875  1conngra  24877  clwlk  24955  clwlkcompim  24966  is2wlkonot  25065  is2spthonot  25066  2wlkonot  25067  2spthonot  25068  2wlkonot3v  25077  2spthonot3v  25078  iseupa  25167  minvecolem4b  25992  minvecolem4  25994  br8d  27678  ressprs  27877  resstos  27882  isomnd  27925  submomnd  27934  ogrpaddltrd  27944  isinftm  27959  isorng  28024  metidv  28106  pstmfval  28110  faeval  28455  brfae  28457  isscon  28935  mclsax  29193  wfrlem5  29587  frrlem5  29631  fnwe2lem2  31236  fnwe2lem3  31237  aomclem8  31246  fperdvper  31954  rngcifuestrc  33059  lcvbr  35143  isopos  35302  cmtvalN  35333  isoml  35360  cvrfval  35390  cvrval  35391  pats  35407  isatl  35421  iscvlat  35445  ishlat1  35474  llnset  35626  lplnset  35650  lvolset  35693  lineset  35859  psubspset  35865  pmapfval  35877  lautset  36203  ldilfset  36229  ltrnfset  36238  trlfset  36282  diaffval  37154  dicffval  37298  dihffval  37354  iunrelexpuztr  38206