Theorem breqd 4427

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 4418	. 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 189   = wceq 1455   class class class wbr 4416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-cleq 2455  df-clel 2458  df-br 4417

This theorem is referenced by:  breq123d  4430  breqdi  4431  sbcbr123  4468  sbcbr  4469  sbcbr12g  4470  fvmptopab1  6359  brfvopab  6363  bropopvvv  6901  bropfvvvvlem  6902  sprmpt2d  6997  wfrlem5  7066  supeq123d  7990  fpwwe2lem12  9092  fpwwe2  9094  brtrclfv  13115  dfrtrclrec2  13169  rtrclreclem3  13172  relexpindlem  13175  shftfib  13184  2shfti  13192  prdsval  15402  pwsle  15439  pwsleval  15440  imasleval  15496  issect  15707  isinv  15714  episect  15739  brcic  15752  ciclcl  15756  cicrcl  15757  isfunc  15818  funcres2c  15855  isfull  15864  isfth  15868  fullpropd  15874  fthpropd  15875  elhoma  15976  isposd  16250  pltval  16255  lubfval  16273  glbfval  16286  joinfval  16296  meetfval  16310  odumeet  16435  odujoin  16437  ipole  16453  eqgval  16915  unitpropd  17974  ltbval  18744  opsrval  18747  znleval  19174  lmbr  20323  metustexhalf  21620  metucn  21635  isphtpc  22074  dvef  22981  taylthlem1  23377  ulmval  23384  iscgrg  24606  legov  24679  ishlg  24696  opphllem5  24842  opphllem6  24843  hpgbr  24851  iscgra  24900  acopy  24923  acopyeu  24924  isinag  24928  isleag  24932  iseqlg  24946  wlkon  25310  iswlkon  25311  wlkonprop  25312  trls  25315  trlon  25319  istrlon  25320  trlonprop  25321  pths  25345  spths  25346  pthon  25354  ispthon  25355  pthonprop  25356  spthon  25361  isspthon  25362  spthonprp  25364  cyclispthon  25410  dfconngra1  25448  isconngra  25449  isconngra1  25450  1conngra  25452  clwlk  25530  clwlkcompim  25541  is2wlkonot  25640  is2spthonot  25641  2wlkonot  25642  2spthonot  25643  2wlkonot3v  25652  2spthonot3v  25653  iseupa  25742  minvecolem4b  26569  minvecolem4  26571  minvecolem4bOLD  26579  minvecolem4OLD  26581  br8d  28267  ressprs  28465  resstos  28470  isomnd  28513  submomnd  28522  ogrpaddltrd  28532  isinftm  28547  isorng  28611  metidv  28744  pstmfval  28748  faeval  29118  brfae  29120  isscon  29998  mclsax  30256  frrlem5  30567  lcvbr  32632  isopos  32791  cmtvalN  32822  isoml  32849  cvrfval  32879  cvrval  32880  pats  32896  isatl  32910  iscvlat  32934  ishlat1  32963  llnset  33115  lplnset  33139  lvolset  33182  lineset  33348  psubspset  33354  pmapfval  33366  lautset  33692  ldilfset  33718  ltrnfset  33727  trlfset  33771  diaffval  34643  dicffval  34787  dihffval  34843  fnwe2lem2  35954  fnwe2lem3  35955  aomclem8  35964  brfvid  36324  brfvidRP  36325  brfvrcld  36328  brfvrcld2  36329  iunrelexpuztr  36356  brtrclfv2  36364  fperdvper  37828  mptmpt2opabbrd  39076  mptmpt2opabovd  39077  wlkbProp  39680  wlkOnprop  39709  1wlksonproplem  39740  istrlson  39742  upgrwlkdvspth  39771  ispthson  39774  isspthson  39775  cyclisPthon  39823  1pthon2v-av  39868  31wlkond  39912  dfconngr1  39929  isconngr  39930  isconngr1  39931  1conngr  39935  rngcifuestrc  40272