Theorem 3brtr3d 5135

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 5115	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷))
5	1, 4	mpbid 235	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103

This theorem is used by:  ofrval  7705  difsnen  9081  domunsncan  9099  infdifsn  9661  ltaddnq  11062  lemul2a  12175  mul2lt0rlt0  13227  xleadd2a  13387  xlemul2a  13422  monoord2  14179  expubnd  14324  bernneq2  14377  hashfun  14585  01sqrexlem2  15415  abs2dif2  15506  rlimdiv  15818  isercolllem1  15837  iseraltlem2  15855  iseraltlem3  15856  fsum00  15970  seqabs  15986  cvgcmp  15988  mertenslem1  16058  fprodle  16168  eftlub  16282  eirrlem  16377  bitscmp  16613  prmreclem1  17099  invisoinvl  17970  chnind  18800  chnlt  18802  chnso  18803  ex-chn1  18816  efgcpbl2  19976  pgpfaclem2  20303  omndadd2d  20349  omndmul2  20352  omndmul3  20353  ogrpinv0le  20355  ogrpaddltbi  20358  ogrpaddltrbid  20360  ogrpinv0lt  20362  gsumle  20364  unitgrp  20618  orngsqr  21128  ornglmulle  21129  orngrmulle  21130  xblss2  24726  xmstri2  24790  mstri2  24791  xmstri  24792  mstri  24793  xmstri3  24794  mstri3  24795  msrtri  24796  nrmmetd  24898  nmtri  24950  nmoi2  25054  xrsxmet  25134  xrge0gsumle  25158  iccpnfhmeo  25271  pcorev2  25354  pi1cpbl  25370  rrxmet  25734  ovoliunlem1  25828  voliunlem3  25878  uniioombllem2  25909  dyadss  25920  dvlipcn  26319  dv11cn  26326  dvle  26332  dvfsumge  26347  dvfsumlem2  26352  dvfsumlem4  26354  dvfsum2  26359  idomrootle  26496  dgrsub  26596  vieta1lem2  26639  itgulm2  26741  radcnvlem1  26745  abelthlem7  26770  efcvx  26781  logdivlti  26953  logcnlem4  26978  logccv  26996  cxple2a  27032  cxpaddlelem  27084  cxpaddle  27085  leibpi  27275  scvxcvx  27318  amgmlem  27322  logdiflbnd  27327  lgamgulmlem2  27362  lgamgulmlem5  27365  lgambdd  27369  lgamcvg2  27387  ftalem2  27406  ppip1le  27493  ppieq0  27508  ppiltx  27509  chpeq0  27540  chtublem  27543  chtub  27544  logexprlim  27557  perfectlem2  27562  bposlem9  27624  2sqlem8  27758  chebbnd1lem1  27801  vmadivsum  27814  rplogsumlem1  27816  dchrisum0re  27845  dchrisum0lem1  27848  selberglem2  27878  chpdifbndlem1  27885  selberg3lem1  27889  pntrlog2bndlem2  27910  pntrlog2bndlem3  27911  pntrlog2bndlem6  27915  pntpbnd2  27919  pntibndlem2  27923  pntlemb  27929  pntlemr  27934  pntlemo  27939  ostth2lem2  27966  ostth2lem3  27967  nosupbnd2lem1  28077  noinfbnd2lem1  28092  mulsgt0  28535  bdayfinbndlem1  28858  tgcgrsub2  29063  legso  29067  krippenlem  29167  midex  29218  opphllem3  29230  trgcopy  29316  perpeqlem  29352  cgraer  29382  cgrabasimass  29383  occllem  31910  nmcexi  32633  cnlnadjlem7  32680  hmopidmchi  32758  oexpled  33473  mgcf1o  33610  isarchi3  33794  archirngz  33796  archiabllem1b  33799  isarchiofld  33806  cos9thpiminplylem1  34460  esum2d  34771  omssubadd  34978  carsgclctun  34999  eulerpartlemgc  35040  dstfrvclim1  35156  fdvneggt  35275  fdvnegge  35277  logdivsqrle  35325  hgt750lemb  35331  subfaclim  36039  ovoliunnfl  38673  itg2addnclem3  38684  ftc1anclem8  38711  cntotbnd  38823  rrnmet  38856  3atlem1  40633  3atlem2  40634  llncvrlpln2  40707  lplncvrlvol2  40765  dalem25  40848  dalawlem7  41027  dalawlem11  41031  cdleme22g  41498  cdlemg18b  41829  cdlemg46  41885  dia2dimlem3  42216  dihord2  42377  3lexlogpow5ineq2  43198  3lexlogpow2ineq1  43201  3lexlogpow5ineq5  43203  aks4d1p1p7  43217  aks4d1p1  43219  aks4d1p6  43224  aks6d1c2lem4  43270  sticksstones6  43294  bcled  43321  bcle2d  43322  aks6d1c7lem1  43323  jm2.24nn  44059  jm2.27a  44105  amgm2d  45291  amgm3d  45292  amgm4d  45293  binomcxplemrat  45427  binomcxplemnotnn0  45433  monoord2xrv  46586  ioossioobi  46622  ioodvbdlimc2lem  47037  stoweidlem10  47113  stoweidlem11  47114  stoweidlem13  47116  stoweidlem14  47117  stoweidlem28  47131  stirlinglem11  47187  stirlinglem12  47188  dirkercncflem4  47209  fourierdlem4  47214  fourierdlem6  47216  fourierdlem11  47221  fourierdlem42  47252  fourierdlem51  47260  fourierdlem73  47282  fourierdlem79  47288  chnerlem2  47986  2pwp1prm  48767  perfectALTVlem2  48913  fllogbd  49765  nnpw2blen  49785  funcoppc4  50353  amgmwlem  51155  amgmlemALT  51156  amgmw2d  51157  young2d  51158