Theorem 3brtr3d 5179

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  ofrval  7684  difsnen  9055  domunsncan  9074  phplem2OLD  9220  infdifsn  9654  ltaddnq  10971  lemul2a  12073  mul2lt0rlt0  13080  xleadd2a  13237  xlemul2a  13272  monoord2  14003  expubnd  14146  bernneq2  14197  hashfun  14401  01sqrexlem2  15194  abs2dif2  15284  rlimdiv  15596  isercolllem1  15615  iseraltlem2  15633  iseraltlem3  15634  fsum00  15748  seqabs  15764  cvgcmp  15766  mertenslem1  15834  fprodle  15944  eftlub  16056  eirrlem  16151  bitscmp  16383  prmreclem1  16853  invisoinvl  17741  efgcpbl2  19666  pgpfaclem2  19993  unitgrp  20274  xblss2  24128  xmstri2  24192  mstri2  24193  xmstri  24194  mstri  24195  xmstri3  24196  mstri3  24197  msrtri  24198  nrmmetd  24303  nmtri  24355  nmoi2  24467  xrsxmet  24545  xrge0gsumle  24569  iccpnfhmeo  24685  pcorev2  24768  pi1cpbl  24784  rrxmet  25149  ovoliunlem1  25243  voliunlem3  25293  uniioombllem2  25324  dyadss  25335  dvlipcn  25735  dv11cn  25742  dvle  25748  dvfsumge  25763  dvfsumlem2  25768  dvfsumlem4  25770  dvfsum2  25775  dgrsub  26010  vieta1lem2  26048  itgulm2  26145  radcnvlem1  26149  abelthlem7  26174  efcvx  26185  logdivlti  26352  logcnlem4  26377  logccv  26395  cxple2a  26431  cxpaddlelem  26483  cxpaddle  26484  leibpi  26671  scvxcvx  26714  amgmlem  26718  logdiflbnd  26723  lgamgulmlem2  26758  lgamgulmlem5  26761  lgambdd  26765  lgamcvg2  26783  ftalem2  26802  ppip1le  26889  ppieq0  26904  ppiltx  26905  chpeq0  26935  chtublem  26938  chtub  26939  logexprlim  26952  perfectlem2  26957  bposlem9  27019  2sqlem8  27153  chebbnd1lem1  27196  vmadivsum  27209  rplogsumlem1  27211  dchrisum0re  27240  dchrisum0lem1  27243  selberglem2  27273  chpdifbndlem1  27280  selberg3lem1  27284  pntrlog2bndlem2  27305  pntrlog2bndlem3  27306  pntrlog2bndlem6  27310  pntpbnd2  27314  pntibndlem2  27318  pntlemb  27324  pntlemr  27329  pntlemo  27334  ostth2lem2  27361  ostth2lem3  27362  nosupbnd2lem1  27442  noinfbnd2lem1  27457  mulsgt0  27827  tgcgrsub2  28101  legso  28105  krippenlem  28196  midex  28243  opphllem3  28255  trgcopy  28310  occllem  30811  nmcexi  31534  cnlnadjlem7  31581  hmopidmchi  31659  mgcf1o  32428  omndadd2d  32484  omndmul2  32488  omndmul3  32489  ogrpinv0le  32491  ogrpaddltbi  32494  ogrpaddltrbid  32496  ogrpinv0lt  32498  gsumle  32500  isarchi3  32591  archirngz  32593  archiabllem1b  32596  orngsqr  32680  ornglmulle  32681  orngrmulle  32682  isarchiofld  32693  esum2d  33377  omssubadd  33585  carsgclctun  33606  eulerpartlemgc  33647  dstfrvclim1  33762  fdvneggt  33898  fdvnegge  33900  logdivsqrle  33948  hgt750lemb  33954  subfaclim  34465  gg-dvfsumlem2  35469  ovoliunnfl  36833  itg2addnclem3  36844  ftc1anclem8  36871  cntotbnd  36967  rrnmet  37000  3atlem1  38657  3atlem2  38658  llncvrlpln2  38731  lplncvrlvol2  38789  dalem25  38872  dalawlem7  39051  dalawlem11  39055  cdleme22g  39522  cdlemg18b  39853  cdlemg46  39909  dia2dimlem3  40240  dihord2  40401  3lexlogpow5ineq2  41226  3lexlogpow2ineq1  41229  3lexlogpow5ineq5  41231  aks4d1p1p7  41245  aks4d1p1  41247  aks4d1p6  41252  sticksstones6  41273  jm2.24nn  42000  jm2.27a  42046  idomrootle  42239  amgm2d  43252  amgm3d  43253  amgm4d  43254  binomcxplemrat  43411  binomcxplemnotnn0  43417  monoord2xrv  44493  ioossioobi  44529  ioodvbdlimc2lem  44949  stoweidlem10  45025  stoweidlem11  45026  stoweidlem13  45028  stoweidlem14  45029  stoweidlem28  45043  stirlinglem11  45099  stirlinglem12  45100  dirkercncflem4  45121  fourierdlem4  45126  fourierdlem6  45128  fourierdlem11  45133  fourierdlem42  45164  fourierdlem51  45172  fourierdlem73  45194  fourierdlem79  45200  2pwp1prm  46556  perfectALTVlem2  46689  fllogbd  47334  nnpw2blen  47354  amgmwlem  47937  amgmlemALT  47938  amgmw2d  47939  young2d  47940