Theorem breq12d 4666

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Hypotheses

Ref	Expression
breq1d.1	|- ( ph -> A = B )
breq12d.2	|- ( ph -> C = D )

Assertion

Ref	Expression
breq12d	|- ( ph -> ( A R C <-> B R D ) )

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- ( ph -> A = B )
2		breq12d.2	. 2 |- ( ph -> C = D )
3		breq12 4658	. 2 |- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> ( A R C <-> B R 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-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  breq123d  4667  3brtr3d  4684  3brtr4d  4685  sbcbr  4707  pocl  5042  csbcnvgALT  5307  cnvpo  5673  sbcfung  5912  isoeq1  6567  isocnv  6580  isotr  6586  caovordig  6839  caovordg  6841  caovord2d  6843  caovord  6845  ofrfval  6905  ofrval  6907  ofrfval2  6915  caofref  6923  fnwelem  7292  fundmeng  8031  xpsneng  8045  xpcomeng  8052  xpdom2g  8056  map2xp  8130  mapdom3  8132  limensuc  8137  infensuc  8138  unxpdom  8167  pssnn  8178  dif1en  8193  unfilem3  8226  unfi  8227  domunfican  8233  fodomfi  8239  marypha1lem  8339  wemaplem1  8451  wemaplem2  8452  wemapwe  8594  dif1card  8833  infxpenlem  8836  pwsdompw  9026  infmap2  9040  sornom  9099  isfin5  9121  isfin6  9122  domtriomlem  9264  axdc2lem  9270  axdclem2  9342  pwcfsdom  9405  cfpwsdom  9406  alephom  9407  fpwwe2lem7  9458  fpwwe2lem9  9460  pwxpndom2  9487  tskcard  9603  ordpipq  9764  adderpqlem  9776  mulerpqlem  9777  mulcanenq  9782  lterpq  9792  ltanq  9793  ltmnq  9794  ltaddnq  9796  ltrnq  9801  archnq  9802  reclem4pr  9872  ltasr  9921  sqgt0sr  9927  axpre-ltadd  9988  axpre-mulgt0  9989  ltadd1  10495  leadd2  10497  ltmul2  10874  lemul2  10876  lemul1a  10877  ltdiv1  10887  ltdiv2  10909  lediv2  10913  div4p1lem1div2  11287  nn0ledivnn  11941  xleadd1  12085  xltadd2  12087  xsubge0  12091  xlemul1a  12118  xlemul1  12120  xlemul2  12121  xltmul2  12123  ltdifltdiv  12635  fzennn  12767  monoord  12831  monoord2  12832  ltexp2r  12917  leexp1a  12919  sqlecan  12971  bernneq  12990  faclbnd  13077  faclbnd3  13079  faclbnd4lem1  13080  faclbnd4lem2  13081  faclbnd4lem3  13082  faclbnd4lem4  13083  faclbnd6  13086  facubnd  13087  rlimcld2  14309  isercoll2  14399  climsup  14400  iseraltlem2  14413  fsumabs  14533  fsumrlim  14543  climcndslem1  14581  climcndslem2  14582  supcvg  14588  geomulcvg  14607  cvgrat  14615  ntrivcvgtail  14632  fprodle  14727  ruclem2  14961  ruclem8  14966  addmodlteqALT  15047  fproddvdsd  15059  sadcaddlem  15179  sadcadd  15180  nn0seqcvgd  15283  algcvg  15289  algcvga  15292  eucalgcvga  15299  isprm5  15419  qnumgt0  15458  pcprendvds2  15546  pcpremul  15548  pcadd2  15594  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  2expltfac  15799  xpsle  16241  mreexexlemd  16304  issubc  16495  latjlej2  17066  latmlem2  17082  sylow1lem3  18015  isslw  18023  fislw  18040  efgi  18132  lt6abl  18296  ablfac1eu  18472  isabv  18819  abvtri  18830  cayleyhamilton1  20697  isucn  22082  ispsmet  22109  psmettri2  22114  ismet  22128  isxmet  22129  xmettri2  22145  imasdsf1olem  22178  imasf1oxmet  22180  blvalps  22190  blval  22191  comet  22318  stdbdxmet  22320  nrmmetd  22379  tngngp  22458  tngngp3  22460  nmofval  22518  nmolb2d  22522  nmoi  22532  nmoix  22533  icopnfhmeo  22742  xrhmeo  22745  evth2  22759  pi1grplem  22849  minveclem6  23205  ovolfiniun  23269  ovoliunlem3  23272  voliunlem3  23320  ioombl1  23330  mbfmax  23416  mbfpos  23418  itg1climres  23481  mbfi1fseqlem2  23483  mbfi1fseqlem6  23487  mbfi1fseq  23488  mbfmullem  23492  itg2split  23516  itg2monolem1  23517  itg2monolem3  23519  itg2mono  23520  itg2i1fseqle  23521  itg2i1fseq  23522  itg2i1fseq2  23523  itg2addlem  23525  rolle  23753  dvlip  23756  c1lip1  23760  dvcnvrelem1  23780  dvcvx  23783  ply1divex  23896  q1pval  23913  fta1glem2  23926  fta1g  23927  fta1b  23929  plydivlem3  24050  fta1lem  24062  fta1  24063  aalioulem3  24089  aalioulem4  24090  aaliou3lem2  24098  aaliou3lem8  24100  aaliou3lem9  24105  ulmdvlem1  24154  ulmdvlem3  24156  abelthlem2  24186  abelthlem7a  24191  argrege0  24357  cxplt  24440  cxplea  24442  cxple2  24443  cxplt3  24446  logbleb  24521  logblt  24522  rlimcxp  24700  scvxcvx  24712  jensenlem2  24714  ftalem3  24801  ftalem7  24805  vmalelog  24930  chtub  24937  chpchtsum  24944  bclbnd  25005  efexple  25006  bposlem5  25013  bposlem6  25014  bposlem7  25015  lgsdilem  25049  2lgslem1a2  25115  dchrisumlem3  25180  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumlema  25189  dchrvmasumiflem1  25190  dchrisum0flblem2  25198  dchrisum0flb  25199  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem2  25207  pntrlog2bndlem2  25267  pntibndlem2  25280  pntlemf  25294  ostth2lem1  25307  qabvle  25314  legso  25494  iscgra  25701  isleag  25733  iseqlg  25747  brbtwn2  25785  axlowdim  25841  ewlksfval  26497  isnvlem  27465  nvtri  27525  nmlnoubi  27651  nmblolbii  27654  nmblolbi  27655  blocnilem  27659  sii  27709  ubthlem2  27727  minvecolem3  27732  minvecolem5  27737  minvecolem6  27738  norm-ii  27995  norm3dif  28007  norm3adifi  28010  bcs  28038  pjnorm  28583  pjnel  28585  nmbdoplbi  28883  nmbdoplb  28884  nmcoplb  28889  lnconi  28892  nmbdfnlb  28909  nmcfnlb  28913  pjdifnormi  29026  mdslmd2i  29189  cvmd  29195  cvexch  29233  cdj1i  29292  cdj3lem1  29293  cdj3lem2b  29296  cdj3lem3b  29299  cdj3i  29300  isoun  29479  isomnd  29701  omndadd  29706  omndmul  29714  ogrpinvlt  29724  isinftm  29735  gsumle  29779  xrmulc1cn  29976  lmdvg  29999  nexple  30071  faeval  30309  brfae  30311  inelcarsg  30373  carsgsigalem  30377  carsgclctunlem2  30381  carsgclctun  30383  hgt750lemc  30725  hgt750lemd  30726  hgt749d  30727  sconnpht  31211  snmlval  31313  lediv2aALT  31571  faclim  31632  poseq  31750  sltval2  31809  sltres  31815  nolesgn2o  31824  nodense  31842  nolt02o  31845  noresle  31846  nosupbnd2lem1  31861  nosupbnd2  31862  fvtransport  32139  idinside  32191  btwnconn1lem7  32200  btwnconn1lem11  32204  btwnconn1lem12  32205  nn0prpwlem  32317  poimirlem29  33438  heicant  33444  itg2addnclem  33461  itg2addnclem3  33463  itg2gt0cn  33465  ftc1anclem6  33490  ftc1anc  33493  ftc2nc  33494  dvasin  33496  areacirclem1  33500  seqpo  33543  incsequz  33544  metf1o  33551  mettrifi  33553  cntotbnd  33595  heiborlem4  33613  heiborlem6  33615  heiborlem10  33619  bfplem1  33621  bfplem2  33622  isopos  34467  oplecon3b  34487  atlatle  34607  4at2  34900  pmaple  35047  islaut  35369  lautcnvle  35375  lautco  35383  ltrncnvel  35428  cdlemeg49lebilem  35827  cdlemg17h  35956  tendoset  36047  tendotp  36049  cdlemk39s  36227  irrapxlem2  37387  irrapxlem4  37389  irrapxlem5  37390  irrapxlem6  37391  pellexlem3  37395  monotuz  37506  monotoddzzfi  37507  monotoddzz  37508  expmordi  37512  jm2.17a  37527  jm2.17b  37528  rmygeid  37531  rmydioph  37581  expdiophlem1  37588  expdiophlem2  37589  ttac  37603  fnwe2lem2  37621  relexp01min  38005  cvgdvgrat  38512  monoords  39511  supxrgelem  39553  supxrge  39554  abslt2sqd  39576  ltmulneg  39615  ltdiv23neg  39617  evthiccabs  39718  sqrlearg  39780  climinf  39838  climinff  39843  limsupres  39937  climinf2  39939  climinf2mpt  39946  climinfmpt  39947  supcnvlimsup  39972  liminfval2  40000  liminflelimsuplem  40007  liminfltlem  40036  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  iblspltprt  40189  itgspltprt  40195  stoweidlem3  40220  fourierdlem2  40326  fourierdlem3  40327  fourierdlem11  40335  fourierdlem12  40336  fourierdlem15  40339  fourierdlem34  40358  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem79  40402  fourierdlem83  40406  fourierdlem89  40412  fourierdlem91  40414  fourierdlem100  40423  fourierdlem107  40430  fourierdlem109  40432  fourierdlem112  40435  etransclem31  40482  etransclem32  40483  rrndistlt  40510  ioorrnopn  40525  ioorrnopnxrlem  40526  sge0less  40609  sge0le  40624  sge0split  40626  sge0lempt  40627  sge0iunmptlemre  40632  sge0isum  40644  sge0seq  40663  meaiuninclem  40697  meaiininclem  40700  meaiininc  40701  isome  40708  omeunile  40719  omeiunlempt  40734  carageniuncllem2  40736  0ome  40743  isomenndlem  40744  isomennd  40745  ovnsslelem  40774  ovnssle  40775  ovnsubadd  40786  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmvval0  40801  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoidmvlelem5  40813  hoidmvle  40814  hoidifhspdmvle  40834  hspmbllem2  40841  hspmbl  40843  ovnsubadd2lem  40859  ovolval4lem2  40864  ovolval4  40865  ovolval5lem2  40867  vonioolem2  40895  vonioo  40896  vonicclem2  40898  vonicc  40899  smfid  40961  smflimlem3  40981  2elfz2melfz  41328  smonoord  41341  iccpart  41352  iccpartimp  41353  iccpartres  41354  sqrtpwpw2p  41450  ismgmALT  41859  iscmgmALT  41860  issgrpALT  41861  iscsgrpALT  41862  lindslinindsimp2lem5  42251  aacllem  42547