Theorem 3brtr3d 5147

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)

Hypotheses

Ref	Expression
3brtr3d.1	⊢ (𝜑 → 𝐴𝑅𝐵)
3brtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3brtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3brtr3d	⊢ (𝜑 → 𝐶𝑅𝐷)

Proof of Theorem 3brtr3d

Step	Hyp	Ref	Expression
1		3brtr3d.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3		3brtr3d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	breq12d 5127	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷))
5	1, 4	mpbid 235	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5114

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115

This theorem is used by:  ofrval  7699  difsnen  9057  domunsncan  9075  infdifsn  9636  ltaddnq  10977  lemul2a  12088  mul2lt0rlt0  13138  xleadd2a  13298  xlemul2a  13333  monoord2  14089  expubnd  14234  bernneq2  14286  hashfun  14494  01sqrexlem2  15320  abs2dif2  15411  rlimdiv  15723  isercolllem1  15742  iseraltlem2  15760  iseraltlem3  15761  fsum00  15876  seqabs  15892  cvgcmp  15894  mertenslem1  15964  fprodle  16076  eftlub  16190  eirrlem  16285  bitscmp  16521  prmreclem1  17001  invisoinvl  17872  chnind  18702  chnlt  18704  chnso  18705  ex-chn1  18718  efgcpbl2  19858  pgpfaclem2  20185  omndadd2d  20231  omndmul2  20234  omndmul3  20235  ogrpinv0le  20237  ogrpaddltbi  20240  ogrpaddltrbid  20242  ogrpinv0lt  20244  gsumle  20246  unitgrp  20498  orngsqr  21006  ornglmulle  21007  orngrmulle  21008  xblss2  24596  xmstri2  24660  mstri2  24661  xmstri  24662  mstri  24663  xmstri3  24664  mstri3  24665  msrtri  24666  nrmmetd  24768  nmtri  24820  nmoi2  24924  xrsxmet  25004  xrge0gsumle  25028  iccpnfhmeo  25141  pcorev2  25224  pi1cpbl  25240  rrxmet  25604  ovoliunlem1  25698  voliunlem3  25748  uniioombllem2  25779  dyadss  25790  dvlipcn  26190  dv11cn  26197  dvle  26203  dvfsumge  26218  dvfsumlem2  26223  dvfsumlem4  26225  dvfsum2  26230  idomrootle  26367  dgrsub  26466  vieta1lem2  26509  itgulm2  26609  radcnvlem1  26613  abelthlem7  26638  efcvx  26649  logdivlti  26822  logcnlem4  26847  logccv  26865  cxple2a  26901  cxpaddlelem  26953  cxpaddle  26954  leibpi  27144  scvxcvx  27187  amgmlem  27191  logdiflbnd  27196  lgamgulmlem2  27231  lgamgulmlem5  27234  lgambdd  27238  lgamcvg2  27256  ftalem2  27275  ppip1le  27362  ppieq0  27377  ppiltx  27378  chpeq0  27409  chtublem  27412  chtub  27413  logexprlim  27426  perfectlem2  27431  bposlem9  27493  2sqlem8  27627  chebbnd1lem1  27670  vmadivsum  27683  rplogsumlem1  27685  dchrisum0re  27714  dchrisum0lem1  27717  selberglem2  27747  chpdifbndlem1  27754  selberg3lem1  27758  pntrlog2bndlem2  27779  pntrlog2bndlem3  27780  pntrlog2bndlem6  27784  pntpbnd2  27788  pntibndlem2  27792  pntlemb  27798  pntlemr  27803  pntlemo  27808  ostth2lem2  27835  ostth2lem3  27836  nosupbnd2lem1  27916  noinfbnd2lem1  27931  mulsgt0  28374  bdayfinbndlem1  28697  tgcgrsub2  28901  legso  28905  krippenlem  29004  midex  29055  opphllem3  29067  trgcopy  29152  perpeqlem  29187  occllem  31692  nmcexi  32415  cnlnadjlem7  32462  hmopidmchi  32540  oexpled  33217  mgcf1o  33354  isarchi3  33538  archirngz  33540  archiabllem1b  33543  isarchiofld  33550  cos9thpiminplylem1  34203  esum2d  34514  omssubadd  34722  carsgclctun  34743  eulerpartlemgc  34784  dstfrvclim1  34900  fdvneggt  35019  fdvnegge  35021  logdivsqrle  35069  hgt750lemb  35075  subfaclim  35701  ovoliunnfl  38354  itg2addnclem3  38365  ftc1anclem8  38392  cntotbnd  38488  rrnmet  38521  3atlem1  40298  3atlem2  40299  llncvrlpln2  40372  lplncvrlvol2  40430  dalem25  40513  dalawlem7  40692  dalawlem11  40696  cdleme22g  41163  cdlemg18b  41494  cdlemg46  41550  dia2dimlem3  41881  dihord2  42042  3lexlogpow5ineq2  42863  3lexlogpow2ineq1  42866  3lexlogpow5ineq5  42868  aks4d1p1p7  42882  aks4d1p1  42884  aks4d1p6  42889  aks6d1c2lem4  42935  sticksstones6  42959  bcled  42986  bcle2d  42987  aks6d1c7lem1  42988  jm2.24nn  43727  jm2.27a  43773  amgm2d  44965  amgm3d  44966  amgm4d  44967  binomcxplemrat  45101  binomcxplemnotnn0  45107  monoord2xrv  46238  ioossioobi  46274  ioodvbdlimc2lem  46689  stoweidlem10  46765  stoweidlem11  46766  stoweidlem13  46768  stoweidlem14  46769  stoweidlem28  46783  stirlinglem11  46839  stirlinglem12  46840  dirkercncflem4  46861  fourierdlem4  46866  fourierdlem6  46868  fourierdlem11  46873  fourierdlem42  46904  fourierdlem51  46912  fourierdlem73  46934  fourierdlem79  46940  chnerlem2  47640  2pwp1prm  48382  perfectALTVlem2  48528  fllogbd  49381  nnpw2blen  49401  funcoppc4  49963  amgmwlem  50691  amgmlemALT  50692  amgmw2d  50693  young2d  50694