Theorem 3brtr3d 5172

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

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

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 2702

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 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142

This theorem is referenced by:  ofrval  7665  difsnen  9036  domunsncan  9055  phplem2OLD  9201  infdifsn  9634  ltaddnq  10951  lemul2a  12051  mul2lt0rlt0  13058  xleadd2a  13215  xlemul2a  13250  monoord2  13981  expubnd  14124  bernneq2  14175  hashfun  14379  01sqrexlem2  15172  abs2dif2  15262  rlimdiv  15574  isercolllem1  15593  iseraltlem2  15611  iseraltlem3  15612  fsum00  15726  seqabs  15742  cvgcmp  15744  mertenslem1  15812  fprodle  15922  eftlub  16034  eirrlem  16129  bitscmp  16361  prmreclem1  16831  invisoinvl  17719  efgcpbl2  19589  pgpfaclem2  19911  unitgrp  20149  xblss2  23837  xmstri2  23901  mstri2  23902  xmstri  23903  mstri  23904  xmstri3  23905  mstri3  23906  msrtri  23907  nrmmetd  24012  nmtri  24064  nmoi2  24176  xrsxmet  24254  xrge0gsumle  24278  iccpnfhmeo  24390  pcorev2  24473  pi1cpbl  24489  rrxmet  24854  ovoliunlem1  24948  voliunlem3  24998  uniioombllem2  25029  dyadss  25040  dvlipcn  25440  dv11cn  25447  dvle  25453  dvfsumge  25468  dvfsumlem2  25473  dvfsumlem4  25475  dvfsum2  25480  dgrsub  25715  vieta1lem2  25753  itgulm2  25850  radcnvlem1  25854  abelthlem7  25879  efcvx  25890  logdivlti  26057  logcnlem4  26082  logccv  26100  cxple2a  26136  cxpaddlelem  26186  cxpaddle  26187  leibpi  26374  scvxcvx  26417  amgmlem  26421  logdiflbnd  26426  lgamgulmlem2  26461  lgamgulmlem5  26464  lgambdd  26468  lgamcvg2  26486  ftalem2  26505  ppip1le  26592  ppieq0  26607  ppiltx  26608  chpeq0  26638  chtublem  26641  chtub  26642  logexprlim  26655  perfectlem2  26660  bposlem9  26722  2sqlem8  26856  chebbnd1lem1  26899  vmadivsum  26912  rplogsumlem1  26914  dchrisum0re  26943  dchrisum0lem1  26946  selberglem2  26976  chpdifbndlem1  26983  selberg3lem1  26987  pntrlog2bndlem2  27008  pntrlog2bndlem3  27009  pntrlog2bndlem6  27013  pntpbnd2  27017  pntibndlem2  27021  pntlemb  27027  pntlemr  27032  pntlemo  27037  ostth2lem2  27064  ostth2lem3  27065  nosupbnd2lem1  27145  noinfbnd2lem1  27160  mulsgt0  27512  tgcgrsub2  27711  legso  27715  krippenlem  27806  midex  27853  opphllem3  27865  trgcopy  27920  occllem  30419  nmcexi  31142  cnlnadjlem7  31189  hmopidmchi  31267  mgcf1o  32044  omndadd2d  32097  omndmul2  32101  omndmul3  32102  ogrpinv0le  32104  ogrpaddltbi  32107  ogrpaddltrbid  32109  ogrpinv0lt  32111  gsumle  32113  isarchi3  32204  archirngz  32206  archiabllem1b  32209  orngsqr  32284  ornglmulle  32285  orngrmulle  32286  isarchiofld  32297  esum2d  32922  omssubadd  33130  carsgclctun  33151  eulerpartlemgc  33192  dstfrvclim1  33307  fdvneggt  33443  fdvnegge  33445  logdivsqrle  33493  hgt750lemb  33499  subfaclim  34010  ovoliunnfl  36334  itg2addnclem3  36345  ftc1anclem8  36372  cntotbnd  36469  rrnmet  36502  3atlem1  38159  3atlem2  38160  llncvrlpln2  38233  lplncvrlvol2  38291  dalem25  38374  dalawlem7  38553  dalawlem11  38557  cdleme22g  39024  cdlemg18b  39355  cdlemg46  39411  dia2dimlem3  39742  dihord2  39903  3lexlogpow5ineq2  40725  3lexlogpow2ineq1  40728  3lexlogpow5ineq5  40730  aks4d1p1p7  40744  aks4d1p1  40746  aks4d1p6  40751  sticksstones6  40772  jm2.24nn  41469  jm2.27a  41515  idomrootle  41708  amgm2d  42721  amgm3d  42722  amgm4d  42723  binomcxplemrat  42880  binomcxplemnotnn0  42886  monoord2xrv  43967  ioossioobi  44003  ioodvbdlimc2lem  44423  stoweidlem10  44499  stoweidlem11  44500  stoweidlem13  44502  stoweidlem14  44503  stoweidlem28  44517  stirlinglem11  44573  stirlinglem12  44574  dirkercncflem4  44595  fourierdlem4  44600  fourierdlem6  44602  fourierdlem11  44607  fourierdlem42  44638  fourierdlem51  44646  fourierdlem73  44668  fourierdlem79  44674  2pwp1prm  46029  perfectALTVlem2  46162  fllogbd  46894  nnpw2blen  46914  amgmwlem  47497  amgmlemALT  47498  amgmw2d  47499  young2d  47500