Theorem breqd 4183

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 4174	. 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 177   = wceq 1649   class class class wbr 4172

This theorem is referenced by:  breq123d  4186  sbcbr12g  4222  bropopvvv  6385  sprmpt2  6435  fpwwe2lem12  8472  fpwwe2  8474  shftfib  11842  2shfti  11850  prdsval  13633  pwsle  13669  pwsleval  13670  imasleval  13721  issect  13934  isinv  13940  episect  13961  isfunc  14016  funcres2c  14053  isfull  14062  isfth  14066  fullpropd  14072  fthpropd  14073  elhoma  14142  isposd  14367  pltval  14372  lubfval  14390  glbfval  14395  ipole  14539  eqgval  14944  unitpropd  15757  ltbval  16487  opsrval  16490  znleval  16790  lmbr  17276  metustexhalfOLD  18546  metustexhalf  18547  metucnOLD  18571  metucn  18572  isphtpc  18972  dvef  19817  taylthlem1  20242  ulmval  20249  wlkon  21483  iswlkon  21484  wlkonprop  21485  trls  21489  trlon  21493  istrlon  21494  trlonprop  21495  pths  21519  spths  21520  pthon  21528  ispthon  21529  pthonprop  21530  spthon  21535  isspthon  21536  spthonprp  21538  cyclispthon  21573  dfconngra1  21611  isconngra  21612  isconngra1  21613  1conngra  21615  iseupa  21640  minvecolem4b  22333  minvecolem4  22335  resstos  24141  isofld  24188  subofld  24198  isinftm  24204  metidv  24240  pstmfval  24244  faeval  24550  brfae  24552  isscon  24866  relexpindlem  25092  dfrtrclrec2  25096  rtrclreclem.trans  25099  wfrlem5  25474  frrlem5  25499  fnwe2lem2  27016  fnwe2lem3  27017  supeq123d  27026  aomclem8  27027  is2wlkonot  28060  is2spthonot  28061  2wlkonot  28062  2spthonot  28063  2wlkonot3v  28072  2spthonot3v  28073  lcvbr  29504  isopos  29663  cmtvalN  29694  isoml  29721  cvrfval  29751  cvrval  29752  pats  29768  isatl  29782  iscvlat  29806  ishlat1  29835  llnset  29987  lplnset  30011  lvolset  30054  lineset  30220  psubspset  30226  pmapfval  30238  lautset  30564  ldilfset  30590  ltrnfset  30599  trlfset  30642  diaffval  31513  dicffval  31657  dihffval  31713

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400  df-br 4173