Theorem breqd 4458

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 4449	. 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 1379   class class class wbr 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462  df-br 4448

This theorem is referenced by:  breq123d  4461  sbcbr123  4498  sbcbr  4500  sbcbr12g  4501  bropopvvv  6863  sprmpt2d  6952  supeq123d  7910  fpwwe2lem12  9019  fpwwe2  9021  shftfib  12868  2shfti  12876  prdsval  14710  pwsle  14747  pwsleval  14748  imasleval  14796  issect  15009  isinv  15015  episect  15036  isfunc  15091  funcres2c  15128  isfull  15137  isfth  15141  fullpropd  15147  fthpropd  15148  elhoma  15217  isposd  15442  pltval  15447  lubfval  15465  glbfval  15478  joinfval  15488  meetfval  15502  odumeet  15627  odujoin  15629  ipole  15645  eqgval  16055  unitpropd  17147  ltbval  17935  opsrval  17938  znleval  18388  lmbr  19553  metustexhalfOLD  20829  metustexhalf  20830  metucnOLD  20854  metucn  20855  isphtpc  21257  dvef  22144  taylthlem1  22530  ulmval  22537  iscgrg  23660  legov  23727  wlkon  24237  iswlkon  24238  wlkonprop  24239  trls  24242  trlon  24246  istrlon  24247  trlonprop  24248  pths  24272  spths  24273  pthon  24281  ispthon  24282  pthonprop  24283  spthon  24288  isspthon  24289  spthonprp  24291  cyclispthon  24337  dfconngra1  24375  isconngra  24376  isconngra1  24377  1conngra  24379  clwlk  24457  clwlkcompim  24468  is2wlkonot  24567  is2spthonot  24568  2wlkonot  24569  2spthonot  24570  2wlkonot3v  24579  2spthonot3v  24580  iseupa  24669  minvecolem4b  25498  minvecolem4  25500  br8d  27164  ressprs  27333  resstos  27338  isomnd  27381  submomnd  27390  ogrpaddltrd  27400  isinftm  27415  archiabllem2a  27428  isorng  27480  metidv  27535  pstmfval  27539  faeval  27886  brfae  27888  isscon  28339  relexpindlem  28565  dfrtrclrec2  28569  rtrclreclem.trans  28572  wfrlem5  28952  frrlem5  28996  fnwe2lem2  30629  fnwe2lem3  30630  aomclem8  30639  fperdvper  31276  lcvbr  33836  isopos  33995  cmtvalN  34026  isoml  34053  cvrfval  34083  cvrval  34084  pats  34100  isatl  34114  iscvlat  34138  ishlat1  34167  llnset  34319  lplnset  34343  lvolset  34386  lineset  34552  psubspset  34558  pmapfval  34570  lautset  34896  ldilfset  34922  ltrnfset  34931  trlfset  34974  diaffval  35845  dicffval  35989  dihffval  36045