Theorem 3brtr3d 5126

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096

This theorem is referenced by:  ofrval  7629  difsnen  8983  domunsncan  9001  infdifsn  9572  ltaddnq  10887  lemul2a  11997  mul2lt0rlt0  13015  xleadd2a  13174  xlemul2a  13209  monoord2  13958  expubnd  14103  bernneq2  14155  hashfun  14362  01sqrexlem2  15168  abs2dif2  15259  rlimdiv  15571  isercolllem1  15590  iseraltlem2  15608  iseraltlem3  15609  fsum00  15723  seqabs  15739  cvgcmp  15741  mertenslem1  15809  fprodle  15921  eftlub  16036  eirrlem  16131  bitscmp  16367  prmreclem1  16846  invisoinvl  17715  efgcpbl2  19654  pgpfaclem2  19981  omndadd2d  20027  omndmul2  20030  omndmul3  20031  ogrpinv0le  20033  ogrpaddltbi  20036  ogrpaddltrbid  20038  ogrpinv0lt  20040  gsumle  20042  unitgrp  20286  orngsqr  20769  ornglmulle  20770  orngrmulle  20771  xblss2  24306  xmstri2  24370  mstri2  24371  xmstri  24372  mstri  24373  xmstri3  24374  mstri3  24375  msrtri  24376  nrmmetd  24478  nmtri  24530  nmoi2  24634  xrsxmet  24714  xrge0gsumle  24738  iccpnfhmeo  24859  pcorev2  24944  pi1cpbl  24960  rrxmet  25324  ovoliunlem1  25419  voliunlem3  25469  uniioombllem2  25500  dyadss  25511  dvlipcn  25915  dv11cn  25922  dvle  25928  dvfsumge  25944  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem4  25952  dvfsum2  25957  idomrootle  26094  dgrsub  26194  vieta1lem2  26235  itgulm2  26334  radcnvlem1  26338  abelthlem7  26364  efcvx  26375  logdivlti  26545  logcnlem4  26570  logccv  26588  cxple2a  26624  cxpaddlelem  26677  cxpaddle  26678  leibpi  26868  scvxcvx  26912  amgmlem  26916  logdiflbnd  26921  lgamgulmlem2  26956  lgamgulmlem5  26959  lgambdd  26963  lgamcvg2  26981  ftalem2  27000  ppip1le  27087  ppieq0  27102  ppiltx  27103  chpeq0  27135  chtublem  27138  chtub  27139  logexprlim  27152  perfectlem2  27157  bposlem9  27219  2sqlem8  27353  chebbnd1lem1  27396  vmadivsum  27409  rplogsumlem1  27411  dchrisum0re  27440  dchrisum0lem1  27443  selberglem2  27473  chpdifbndlem1  27480  selberg3lem1  27484  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem6  27510  pntpbnd2  27514  pntibndlem2  27518  pntlemb  27524  pntlemr  27529  pntlemo  27534  ostth2lem2  27561  ostth2lem3  27562  nosupbnd2lem1  27643  noinfbnd2lem1  27658  mulsgt0  28070  tgcgrsub2  28558  legso  28562  krippenlem  28653  midex  28700  opphllem3  28712  trgcopy  28767  occllem  31265  nmcexi  31988  cnlnadjlem7  32035  hmopidmchi  32113  oexpled  32805  mgcf1o  32958  chnind  32966  chnlt  32968  chnso  32969  isarchi3  33139  archirngz  33141  archiabllem1b  33144  isarchiofld  33151  cos9thpiminplylem1  33748  esum2d  34059  omssubadd  34267  carsgclctun  34288  eulerpartlemgc  34329  dstfrvclim1  34445  fdvneggt  34567  fdvnegge  34569  logdivsqrle  34617  hgt750lemb  34623  subfaclim  35160  ovoliunnfl  37641  itg2addnclem3  37652  ftc1anclem8  37679  cntotbnd  37775  rrnmet  37808  3atlem1  39462  3atlem2  39463  llncvrlpln2  39536  lplncvrlvol2  39594  dalem25  39677  dalawlem7  39856  dalawlem11  39860  cdleme22g  40327  cdlemg18b  40658  cdlemg46  40714  dia2dimlem3  41045  dihord2  41206  3lexlogpow5ineq2  42028  3lexlogpow2ineq1  42031  3lexlogpow5ineq5  42033  aks4d1p1p7  42047  aks4d1p1  42049  aks4d1p6  42054  aks6d1c2lem4  42100  sticksstones6  42124  bcled  42151  bcle2d  42152  aks6d1c7lem1  42153  jm2.24nn  42932  jm2.27a  42978  amgm2d  44171  amgm3d  44172  amgm4d  44173  binomcxplemrat  44323  binomcxplemnotnn0  44329  monoord2xrv  45463  ioossioobi  45499  ioodvbdlimc2lem  45916  stoweidlem10  45992  stoweidlem11  45993  stoweidlem13  45995  stoweidlem14  45996  stoweidlem28  46010  stirlinglem11  46066  stirlinglem12  46067  dirkercncflem4  46088  fourierdlem4  46093  fourierdlem6  46095  fourierdlem11  46100  fourierdlem42  46131  fourierdlem51  46139  fourierdlem73  46161  fourierdlem79  46167  2pwp1prm  47574  perfectALTVlem2  47707  fllogbd  48546  nnpw2blen  48566  funcoppc4  49130  amgmwlem  49788  amgmlemALT  49789  amgmw2d  49790  young2d  49791