Theorem breqd 4664

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 4655	. 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 196   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618  df-br 4654

This theorem is referenced by:  breq123d  4667  breqdi  4668  sbcbr123  4706  sbcbr  4707  sbcbr12g  4708  fvmptopab  6697  brfvopab  6700  mptmpt2opabbrd  7248  mptmpt2opabovd  7249  bropopvvv  7255  bropfvvvvlem  7256  sprmpt2d  7350  wfrlem5  7419  supeq123d  8356  fpwwe2lem12  9463  fpwwe2  9465  brtrclfv  13743  dfrtrclrec2  13797  rtrclreclem3  13800  relexpindlem  13803  shftfib  13812  2shfti  13820  prdsval  16115  pwsle  16152  pwsleval  16153  imasleval  16201  issect  16413  isinv  16420  episect  16445  brcic  16458  ciclcl  16462  cicrcl  16463  isfunc  16524  funcres2c  16561  isfull  16570  isfth  16574  fullpropd  16580  fthpropd  16581  elhoma  16682  isposd  16955  pltval  16960  lubfval  16978  glbfval  16991  joinfval  17001  meetfval  17015  odumeet  17140  odujoin  17142  ipole  17158  eqgval  17643  unitpropd  18697  ltbval  19471  opsrval  19474  znleval  19903  lmbr  21062  metustexhalf  22361  metucn  22376  isphtpc  22793  dvef  23743  taylthlem1  24127  ulmval  24134  iscgrg  25407  legov  25480  ishlg  25497  opphllem5  25643  opphllem6  25644  hpgbr  25652  iscgra  25701  acopy  25724  acopyeu  25725  isinag  25729  isleag  25733  iseqlg  25747  wlkonprop  26554  wksonproplem  26601  istrlson  26603  upgrwlkdvspth  26635  ispthson  26638  isspthson  26639  cyclispthon  26696  wspthsn  26735  wspthsnon  26739  iswspthsnon  26741  1pthon2v  27013  3wlkond  27031  dfconngr1  27048  isconngr  27049  isconngr1  27050  1conngr  27054  conngrv2edg  27055  minvecolem4b  27734  minvecolem4  27736  br8d  29422  ressprs  29655  resstos  29660  isomnd  29701  submomnd  29710  ogrpaddltrd  29720  isinftm  29735  isorng  29799  metidv  29935  pstmfval  29939  faeval  30309  brfae  30311  issconn  31208  mclsax  31466  frrlem5  31784  unceq  33386  alrmomo2  34124  lcvbr  34308  isopos  34467  cmtvalN  34498  isoml  34525  cvrfval  34555  cvrval  34556  pats  34572  isatl  34586  iscvlat  34610  ishlat1  34639  llnset  34791  lplnset  34815  lvolset  34858  lineset  35024  psubspset  35030  pmapfval  35042  lautset  35368  ldilfset  35394  ltrnfset  35403  trlfset  35447  diaffval  36319  dicffval  36463  dihffval  36519  fnwe2lem2  37621  fnwe2lem3  37622  aomclem8  37631  brfvid  37979  brfvidRP  37980  brfvrcld  37983  brfvrcld2  37984  iunrelexpuztr  38011  brtrclfv2  38019  neicvgnvor  38414  neicvgel1  38417  fperdvper  40133  upwlkbprop  41719  rngcifuestrc  41997