Theorem 3brtr3d 5130

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

Syntax hints:   → wi 4   = wceq 1559   class class class wbr 5099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  ofrval  7668  difsnen  9027  domunsncan  9045  infdifsn  9609  ltaddnq  10929  lemul2a  12043  mul2lt0rlt0  13094  xleadd2a  13254  xlemul2a  13289  monoord2  14043  expubnd  14188  bernneq2  14240  hashfun  14447  01sqrexlem2  15253  abs2dif2  15344  rlimdiv  15656  isercolllem1  15675  iseraltlem2  15693  iseraltlem3  15694  fsum00  15809  seqabs  15825  cvgcmp  15827  mertenslem1  15897  fprodle  16009  eftlub  16124  eirrlem  16219  bitscmp  16455  prmreclem1  16935  invisoinvl  17806  chnind  18636  chnlt  18638  chnso  18639  ex-chn1  18652  efgcpbl2  19780  pgpfaclem2  20107  omndadd2d  20153  omndmul2  20156  omndmul3  20157  ogrpinv0le  20159  ogrpaddltbi  20162  ogrpaddltrbid  20164  ogrpinv0lt  20166  gsumle  20168  unitgrp  20411  orngsqr  20895  ornglmulle  20896  orngrmulle  20897  xblss2  24442  xmstri2  24506  mstri2  24507  xmstri  24508  mstri  24509  xmstri3  24510  mstri3  24511  msrtri  24512  nrmmetd  24614  nmtri  24666  nmoi2  24770  xrsxmet  24850  xrge0gsumle  24874  iccpnfhmeo  24987  pcorev2  25070  pi1cpbl  25086  rrxmet  25450  ovoliunlem1  25544  voliunlem3  25594  uniioombllem2  25625  dyadss  25636  dvlipcn  26036  dv11cn  26043  dvle  26049  dvfsumge  26064  dvfsumlem2  26069  dvfsumlem4  26071  dvfsum2  26076  idomrootle  26213  dgrsub  26312  vieta1lem2  26352  itgulm2  26449  radcnvlem1  26453  abelthlem7  26478  efcvx  26489  logdivlti  26662  logcnlem4  26687  logccv  26705  cxple2a  26741  cxpaddlelem  26793  cxpaddle  26794  leibpi  26984  scvxcvx  27027  amgmlem  27031  logdiflbnd  27036  lgamgulmlem2  27071  lgamgulmlem5  27074  lgambdd  27078  lgamcvg2  27096  ftalem2  27115  ppip1le  27202  ppieq0  27217  ppiltx  27218  chpeq0  27249  chtublem  27252  chtub  27253  logexprlim  27266  perfectlem2  27271  bposlem9  27333  2sqlem8  27467  chebbnd1lem1  27510  vmadivsum  27523  rplogsumlem1  27525  dchrisum0re  27554  dchrisum0lem1  27557  selberglem2  27587  chpdifbndlem1  27594  selberg3lem1  27598  pntrlog2bndlem2  27619  pntrlog2bndlem3  27620  pntrlog2bndlem6  27624  pntpbnd2  27628  pntibndlem2  27632  pntlemb  27638  pntlemr  27643  pntlemo  27648  ostth2lem2  27675  ostth2lem3  27676  nosupbnd2lem1  27756  noinfbnd2lem1  27771  mulsgt0  28214  bdayfinbndlem1  28537  tgcgrsub2  28741  legso  28745  krippenlem  28836  midex  28883  opphllem3  28895  trgcopy  28950  occllem  31452  nmcexi  32175  cnlnadjlem7  32222  hmopidmchi  32300  oexpled  32999  mgcf1o  33142  isarchi3  33328  archirngz  33330  archiabllem1b  33333  isarchiofld  33340  cos9thpiminplylem1  34040  esum2d  34351  omssubadd  34558  carsgclctun  34579  eulerpartlemgc  34620  dstfrvclim1  34736  fdvneggt  34858  fdvnegge  34860  logdivsqrle  34908  hgt750lemb  34914  subfaclim  35502  ovoliunnfl  38125  itg2addnclem3  38136  ftc1anclem8  38163  cntotbnd  38259  rrnmet  38292  3atlem1  40071  3atlem2  40072  llncvrlpln2  40145  lplncvrlvol2  40203  dalem25  40286  dalawlem7  40465  dalawlem11  40469  cdleme22g  40936  cdlemg18b  41267  cdlemg46  41323  dia2dimlem3  41654  dihord2  41815  3lexlogpow5ineq2  42636  3lexlogpow2ineq1  42639  3lexlogpow5ineq5  42641  aks4d1p1p7  42655  aks4d1p1  42657  aks4d1p6  42662  aks6d1c2lem4  42708  sticksstones6  42732  bcled  42759  bcle2d  42760  aks6d1c7lem1  42761  jm2.24nn  43500  jm2.27a  43546  amgm2d  44738  amgm3d  44739  amgm4d  44740  binomcxplemrat  44890  binomcxplemnotnn0  44896  monoord2xrv  46021  ioossioobi  46057  ioodvbdlimc2lem  46472  stoweidlem10  46548  stoweidlem11  46549  stoweidlem13  46551  stoweidlem14  46552  stoweidlem28  46566  stirlinglem11  46622  stirlinglem12  46623  dirkercncflem4  46644  fourierdlem4  46649  fourierdlem6  46651  fourierdlem11  46656  fourierdlem42  46687  fourierdlem51  46695  fourierdlem73  46717  fourierdlem79  46723  chnerlem2  47423  2pwp1prm  48162  perfectALTVlem2  48308  fllogbd  49146  nnpw2blen  49166  funcoppc4  49729  amgmwlem  50387  amgmlemALT  50388  amgmw2d  50389  young2d  50390