Theorem breqd 4302

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 4293	. 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 1369   class class class wbr 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2435  df-clel 2438  df-br 4292

This theorem is referenced by:  breq123d  4305  sbcbr123  4342  sbcbr  4344  sbcbr12g  4345  bropopvvv  6652  sprmpt2d  6741  supeq123d  7699  fpwwe2lem12  8807  fpwwe2  8809  shftfib  12560  2shfti  12568  prdsval  14392  pwsle  14429  pwsleval  14430  imasleval  14478  issect  14691  isinv  14697  episect  14718  isfunc  14773  funcres2c  14810  isfull  14819  isfth  14823  fullpropd  14829  fthpropd  14830  elhoma  14899  isposd  15124  pltval  15129  lubfval  15147  glbfval  15160  joinfval  15170  meetfval  15184  odumeet  15309  odujoin  15311  ipole  15327  eqgval  15729  unitpropd  16788  ltbval  17552  opsrval  17555  znleval  17986  lmbr  18861  metustexhalfOLD  20137  metustexhalf  20138  metucnOLD  20162  metucn  20163  isphtpc  20565  dvef  21451  taylthlem1  21837  ulmval  21844  iscgrg  22964  legov  23015  wlkon  23428  iswlkon  23429  wlkonprop  23430  trls  23434  trlon  23438  istrlon  23439  trlonprop  23440  pths  23464  spths  23465  pthon  23473  ispthon  23474  pthonprop  23475  spthon  23480  isspthon  23481  spthonprp  23483  cyclispthon  23518  dfconngra1  23556  isconngra  23557  isconngra1  23558  1conngra  23560  iseupa  23585  minvecolem4b  24278  minvecolem4  24280  br8d  25941  ressprs  26115  resstos  26120  isomnd  26163  submomnd  26172  ogrpaddltrd  26182  isinftm  26197  archiabllem2a  26210  isorng  26266  metidv  26318  pstmfval  26322  faeval  26661  brfae  26663  isscon  27114  relexpindlem  27340  dfrtrclrec2  27344  rtrclreclem.trans  27347  wfrlem5  27727  frrlem5  27771  fnwe2lem2  29402  fnwe2lem3  29403  aomclem8  29412  is2wlkonot  30380  is2spthonot  30381  2wlkonot  30382  2spthonot  30383  2wlkonot3v  30392  2spthonot3v  30393  clwlk  30416  clwlkcompim  30425  lcvbr  32664  isopos  32823  cmtvalN  32854  isoml  32881  cvrfval  32911  cvrval  32912  pats  32928  isatl  32942  iscvlat  32966  ishlat1  32995  llnset  33147  lplnset  33171  lvolset  33214  lineset  33380  psubspset  33386  pmapfval  33398  lautset  33724  ldilfset  33750  ltrnfset  33759  trlfset  33802  diaffval  34673  dicffval  34817  dihffval  34873