Theorem breqd 4437

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 4428	. 2 |- ( A = B -> ( C A D <-> C B D ) )
3	1, 2	syl 17	1 |- ( ph -> ( C A D <-> C B D ) )

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   class class class wbr 4426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2421  df-clel 2424  df-br 4427

This theorem is referenced by:  breq123d  4440  sbcbr123  4477  sbcbr  4478  sbcbr12g  4479  bropopvvv  6887  sprmpt2d  6978  wfrlem5  7048  supeq123d  7970  fpwwe2lem12  9065  fpwwe2  9067  brtrclfv  13045  dfrtrclrec2  13099  rtrclreclem3  13102  relexpindlem  13105  shftfib  13114  2shfti  13122  prdsval  15312  pwsle  15349  pwsleval  15350  imasleval  15398  issect  15609  isinv  15616  episect  15641  brcic  15654  ciclcl  15658  cicrcl  15659  isfunc  15720  funcres2c  15757  isfull  15766  isfth  15770  fullpropd  15776  fthpropd  15777  elhoma  15878  isposd  16152  pltval  16157  lubfval  16175  glbfval  16188  joinfval  16198  meetfval  16212  odumeet  16337  odujoin  16339  ipole  16355  eqgval  16817  unitpropd  17860  ltbval  18630  opsrval  18633  znleval  19056  lmbr  20205  metustexhalf  21502  metucn  21517  isphtpc  21918  dvef  22809  taylthlem1  23193  ulmval  23200  iscgrg  24420  legov  24490  ishlg  24507  opphllem5  24650  opphllem6  24651  hpgbr  24658  iscgra  24707  acopy  24727  acopyeu  24728  isinag  24732  wlkon  25106  iswlkon  25107  wlkonprop  25108  trls  25111  trlon  25115  istrlon  25116  trlonprop  25117  pths  25141  spths  25142  pthon  25150  ispthon  25151  pthonprop  25152  spthon  25157  isspthon  25158  spthonprp  25160  cyclispthon  25206  dfconngra1  25244  isconngra  25245  isconngra1  25246  1conngra  25248  clwlk  25326  clwlkcompim  25337  is2wlkonot  25436  is2spthonot  25437  2wlkonot  25438  2spthonot  25439  2wlkonot3v  25448  2spthonot3v  25449  iseupa  25538  minvecolem4b  26365  minvecolem4  26367  br8d  28057  ressprs  28254  resstos  28259  isomnd  28302  submomnd  28311  ogrpaddltrd  28321  isinftm  28336  isorng  28401  metidv  28534  pstmfval  28538  faeval  28908  brfae  28910  isscon  29737  mclsax  29995  frrlem5  30305  lcvbr  32296  isopos  32455  cmtvalN  32486  isoml  32513  cvrfval  32543  cvrval  32544  pats  32560  isatl  32574  iscvlat  32598  ishlat1  32627  llnset  32779  lplnset  32803  lvolset  32846  lineset  33012  psubspset  33018  pmapfval  33030  lautset  33356  ldilfset  33382  ltrnfset  33391  trlfset  33435  diaffval  34307  dicffval  34451  dihffval  34507  fnwe2lem2  35615  fnwe2lem3  35616  aomclem8  35625  brfvid  35918  brfvidRP  35919  brfvrcld  35922  brfvrcld2  35923  iunrelexpuztr  35950  brtrclfv2  35958  fperdvper  37362  rngcifuestrc  38757