Theorem 3brtr3d 5136

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

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

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  ofrval  7694  difsnen  9062  domunsncan  9080  infdifsn  9642  ltaddnq  11040  lemul2a  12153  mul2lt0rlt0  13205  xleadd2a  13365  xlemul2a  13400  monoord2  14156  expubnd  14301  bernneq2  14354  hashfun  14562  01sqrexlem2  15390  abs2dif2  15481  rlimdiv  15793  isercolllem1  15812  iseraltlem2  15830  iseraltlem3  15831  fsum00  15945  seqabs  15961  cvgcmp  15963  mertenslem1  16033  fprodle  16143  eftlub  16257  eirrlem  16352  bitscmp  16588  prmreclem1  17074  invisoinvl  17945  chnind  18775  chnlt  18777  chnso  18778  ex-chn1  18791  efgcpbl2  19951  pgpfaclem2  20278  omndadd2d  20324  omndmul2  20327  omndmul3  20328  ogrpinv0le  20330  ogrpaddltbi  20333  ogrpaddltrbid  20335  ogrpinv0lt  20337  gsumle  20339  unitgrp  20593  orngsqr  21103  ornglmulle  21104  orngrmulle  21105  xblss2  24701  xmstri2  24765  mstri2  24766  xmstri  24767  mstri  24768  xmstri3  24769  mstri3  24770  msrtri  24771  nrmmetd  24873  nmtri  24925  nmoi2  25029  xrsxmet  25109  xrge0gsumle  25133  iccpnfhmeo  25246  pcorev2  25329  pi1cpbl  25345  rrxmet  25709  ovoliunlem1  25803  voliunlem3  25853  uniioombllem2  25884  dyadss  25895  dvlipcn  26294  dv11cn  26301  dvle  26307  dvfsumge  26322  dvfsumlem2  26327  dvfsumlem4  26329  dvfsum2  26334  idomrootle  26471  dgrsub  26571  vieta1lem2  26616  itgulm2  26718  radcnvlem1  26722  abelthlem7  26747  efcvx  26758  logdivlti  26930  logcnlem4  26955  logccv  26973  cxple2a  27009  cxpaddlelem  27061  cxpaddle  27062  leibpi  27252  scvxcvx  27295  amgmlem  27299  logdiflbnd  27304  lgamgulmlem2  27339  lgamgulmlem5  27342  lgambdd  27346  lgamcvg2  27364  ftalem2  27383  ppip1le  27470  ppieq0  27485  ppiltx  27486  chpeq0  27517  chtublem  27520  chtub  27521  logexprlim  27534  perfectlem2  27539  bposlem9  27601  2sqlem8  27735  chebbnd1lem1  27778  vmadivsum  27791  rplogsumlem1  27793  dchrisum0re  27822  dchrisum0lem1  27825  selberglem2  27855  chpdifbndlem1  27862  selberg3lem1  27866  pntrlog2bndlem2  27887  pntrlog2bndlem3  27888  pntrlog2bndlem6  27892  pntpbnd2  27896  pntibndlem2  27900  pntlemb  27906  pntlemr  27911  pntlemo  27916  ostth2lem2  27943  ostth2lem3  27944  nosupbnd2lem1  28054  noinfbnd2lem1  28069  mulsgt0  28512  bdayfinbndlem1  28835  tgcgrsub2  29040  legso  29044  krippenlem  29144  midex  29195  opphllem3  29207  trgcopy  29293  perpeqlem  29329  cgraer  29359  cgrabasimass  29360  occllem  31887  nmcexi  32610  cnlnadjlem7  32657  hmopidmchi  32735  oexpled  33409  mgcf1o  33546  isarchi3  33730  archirngz  33732  archiabllem1b  33735  isarchiofld  33742  cos9thpiminplylem1  34396  esum2d  34707  omssubadd  34915  carsgclctun  34936  eulerpartlemgc  34977  dstfrvclim1  35093  fdvneggt  35212  fdvnegge  35214  logdivsqrle  35262  hgt750lemb  35268  subfaclim  35922  ovoliunnfl  38548  itg2addnclem3  38559  ftc1anclem8  38586  cntotbnd  38698  rrnmet  38731  3atlem1  40508  3atlem2  40509  llncvrlpln2  40582  lplncvrlvol2  40640  dalem25  40723  dalawlem7  40902  dalawlem11  40906  cdleme22g  41373  cdlemg18b  41704  cdlemg46  41760  dia2dimlem3  42091  dihord2  42252  3lexlogpow5ineq2  43073  3lexlogpow2ineq1  43076  3lexlogpow5ineq5  43078  aks4d1p1p7  43092  aks4d1p1  43094  aks4d1p6  43099  aks6d1c2lem4  43145  sticksstones6  43169  bcled  43196  bcle2d  43197  aks6d1c7lem1  43198  jm2.24nn  43919  jm2.27a  43965  amgm2d  45157  amgm3d  45158  amgm4d  45159  binomcxplemrat  45293  binomcxplemnotnn0  45299  monoord2xrv  46437  ioossioobi  46473  ioodvbdlimc2lem  46888  stoweidlem10  46964  stoweidlem11  46965  stoweidlem13  46967  stoweidlem14  46968  stoweidlem28  46982  stirlinglem11  47038  stirlinglem12  47039  dirkercncflem4  47060  fourierdlem4  47065  fourierdlem6  47067  fourierdlem11  47072  fourierdlem42  47103  fourierdlem51  47111  fourierdlem73  47133  fourierdlem79  47139  chnerlem2  47837  2pwp1prm  48618  perfectALTVlem2  48764  fllogbd  49616  nnpw2blen  49636  funcoppc4  50196  amgmwlem  50931  amgmlemALT  50932  amgmw2d  50933  young2d  50934