Theorem breqd 4291

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 4282	. 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 1362   class class class wbr 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429  df-br 4281

This theorem is referenced by:  breq123d  4294  sbcbr123  4331  sbcbr  4333  sbcbr12g  4334  bropopvvv  6642  sprmpt2d  6731  supeq123d  7688  fpwwe2lem12  8795  fpwwe2  8797  shftfib  12544  2shfti  12552  prdsval  14375  pwsle  14412  pwsleval  14413  imasleval  14461  issect  14674  isinv  14680  episect  14701  isfunc  14756  funcres2c  14793  isfull  14802  isfth  14806  fullpropd  14812  fthpropd  14813  elhoma  14882  isposd  15107  pltval  15112  lubfval  15130  glbfval  15143  joinfval  15153  meetfval  15167  odumeet  15292  odujoin  15294  ipole  15310  eqgval  15709  unitpropd  16722  ltbval  17484  opsrval  17487  znleval  17828  lmbr  18703  metustexhalfOLD  19979  metustexhalf  19980  metucnOLD  20004  metucn  20005  isphtpc  20407  dvef  21293  taylthlem1  21722  ulmval  21729  iscgrg  22845  legov  22891  wlkon  23251  iswlkon  23252  wlkonprop  23253  trls  23257  trlon  23261  istrlon  23262  trlonprop  23263  pths  23287  spths  23288  pthon  23296  ispthon  23297  pthonprop  23298  spthon  23303  isspthon  23304  spthonprp  23306  cyclispthon  23341  dfconngra1  23379  isconngra  23380  isconngra1  23381  1conngra  23383  iseupa  23408  minvecolem4b  24101  minvecolem4  24103  br8d  25765  ressprs  25938  resstos  25943  isomnd  25987  submomnd  25996  ogrpaddltrd  26006  isinftm  26021  archiabllem2a  26034  isorng  26119  metidv  26172  pstmfval  26176  faeval  26515  brfae  26517  isscon  26962  relexpindlem  27187  dfrtrclrec2  27191  rtrclreclem.trans  27194  wfrlem5  27574  frrlem5  27618  fnwe2lem2  29246  fnwe2lem3  29247  aomclem8  29256  is2wlkonot  30225  is2spthonot  30226  2wlkonot  30227  2spthonot  30228  2wlkonot3v  30237  2spthonot3v  30238  clwlk  30261  clwlkcompim  30270  lcvbr  32236  isopos  32395  cmtvalN  32426  isoml  32453  cvrfval  32483  cvrval  32484  pats  32500  isatl  32514  iscvlat  32538  ishlat1  32567  llnset  32719  lplnset  32743  lvolset  32786  lineset  32952  psubspset  32958  pmapfval  32970  lautset  33296  ldilfset  33322  ltrnfset  33331  trlfset  33374  diaffval  34245  dicffval  34389  dihffval  34445