Theorem 3brtr3d 5101

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  ofrval  7523  difsnen  8794  domunsncan  8812  phplem2  8893  infdifsn  9345  ltaddnq  10661  lemul2a  11760  mul2lt0rlt0  12761  xleadd2a  12917  xlemul2a  12952  monoord2  13682  expubnd  13823  bernneq2  13873  hashfun  14080  sqrlem2  14883  abs2dif2  14973  rlimdiv  15285  isercolllem1  15304  iseraltlem2  15322  iseraltlem3  15323  fsum00  15438  seqabs  15454  cvgcmp  15456  mertenslem1  15524  fprodle  15634  eftlub  15746  eirrlem  15841  bitscmp  16073  prmreclem1  16545  invisoinvl  17419  efgcpbl2  19278  pgpfaclem2  19600  unitgrp  19824  xblss2  23463  xmstri2  23527  mstri2  23528  xmstri  23529  mstri  23530  xmstri3  23531  mstri3  23532  msrtri  23533  nrmmetd  23636  nmtri  23688  nmoi2  23800  xrsxmet  23878  xrge0gsumle  23902  iccpnfhmeo  24014  pcorev2  24097  pi1cpbl  24113  rrxmet  24477  ovoliunlem1  24571  voliunlem3  24621  uniioombllem2  24652  dyadss  24663  dvlipcn  25063  dv11cn  25070  dvle  25076  dvfsumge  25091  dvfsumlem2  25096  dvfsumlem4  25098  dvfsum2  25103  dgrsub  25338  vieta1lem2  25376  itgulm2  25473  radcnvlem1  25477  abelthlem7  25502  efcvx  25513  logdivlti  25680  logcnlem4  25705  logccv  25723  cxple2a  25759  cxpaddlelem  25809  cxpaddle  25810  leibpi  25997  scvxcvx  26040  amgmlem  26044  logdiflbnd  26049  lgamgulmlem2  26084  lgamgulmlem5  26087  lgambdd  26091  lgamcvg2  26109  ftalem2  26128  ppip1le  26215  ppieq0  26230  ppiltx  26231  chpeq0  26261  chtublem  26264  chtub  26265  logexprlim  26278  perfectlem2  26283  bposlem9  26345  2sqlem8  26479  chebbnd1lem1  26522  vmadivsum  26535  rplogsumlem1  26537  dchrisum0re  26566  dchrisum0lem1  26569  selberglem2  26599  chpdifbndlem1  26606  selberg3lem1  26610  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem6  26636  pntpbnd2  26640  pntibndlem2  26644  pntlemb  26650  pntlemr  26655  pntlemo  26660  ostth2lem2  26687  ostth2lem3  26688  tgcgrsub2  26860  legso  26864  krippenlem  26955  midex  27002  opphllem3  27014  trgcopy  27069  occllem  29566  nmcexi  30289  cnlnadjlem7  30336  hmopidmchi  30414  mgcf1o  31183  omndadd2d  31236  omndmul2  31240  omndmul3  31241  ogrpinv0le  31243  ogrpaddltbi  31246  ogrpaddltrbid  31248  ogrpinv0lt  31250  gsumle  31252  isarchi3  31343  archirngz  31345  archiabllem1b  31348  orngsqr  31405  ornglmulle  31406  orngrmulle  31407  isarchiofld  31418  esum2d  31961  omssubadd  32167  carsgclctun  32188  eulerpartlemgc  32229  dstfrvclim1  32344  fdvneggt  32480  fdvnegge  32482  logdivsqrle  32530  hgt750lemb  32536  subfaclim  33050  nosupbnd2lem1  33845  noinfbnd2lem1  33860  ovoliunnfl  35746  itg2addnclem3  35757  ftc1anclem8  35784  cntotbnd  35881  rrnmet  35914  3atlem1  37424  3atlem2  37425  llncvrlpln2  37498  lplncvrlvol2  37556  dalem25  37639  dalawlem7  37818  dalawlem11  37822  cdleme22g  38289  cdlemg18b  38620  cdlemg46  38676  dia2dimlem3  39007  dihord2  39168  3lexlogpow5ineq2  39991  3lexlogpow2ineq1  39994  3lexlogpow5ineq5  39996  aks4d1p1p7  40010  aks4d1p1  40012  aks4d1p6  40017  sticksstones6  40035  jm2.24nn  40697  jm2.27a  40743  idomrootle  40936  amgm2d  41698  amgm3d  41699  amgm4d  41700  binomcxplemrat  41857  binomcxplemnotnn0  41863  monoord2xrv  42914  ioossioobi  42945  ioodvbdlimc2lem  43365  stoweidlem10  43441  stoweidlem11  43442  stoweidlem13  43444  stoweidlem14  43445  stoweidlem28  43459  stirlinglem11  43515  stirlinglem12  43516  dirkercncflem4  43537  fourierdlem4  43542  fourierdlem6  43544  fourierdlem11  43549  fourierdlem42  43580  fourierdlem51  43588  fourierdlem73  43610  fourierdlem79  43616  2pwp1prm  44929  perfectALTVlem2  45062  fllogbd  45794  nnpw2blen  45814  amgmwlem  46392  amgmlemALT  46393  amgmw2d  46394  young2d  46395