Theorem 3brtr3d 5178

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

Syntax hints:   → wi 4   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  ofrval  7708  difsnen  9091  domunsncan  9110  phplem2OLD  9252  infdifsn  9694  ltaddnq  11011  lemul2a  12119  mul2lt0rlt0  13134  xleadd2a  13292  xlemul2a  13327  monoord2  14070  expubnd  14213  bernneq2  14265  hashfun  14472  01sqrexlem2  15278  abs2dif2  15368  rlimdiv  15678  isercolllem1  15697  iseraltlem2  15715  iseraltlem3  15716  fsum00  15830  seqabs  15846  cvgcmp  15848  mertenslem1  15916  fprodle  16028  eftlub  16141  eirrlem  16236  bitscmp  16471  prmreclem1  16949  invisoinvl  17837  efgcpbl2  19789  pgpfaclem2  20116  unitgrp  20399  xblss2  24427  xmstri2  24491  mstri2  24492  xmstri  24493  mstri  24494  xmstri3  24495  mstri3  24496  msrtri  24497  nrmmetd  24602  nmtri  24654  nmoi2  24766  xrsxmet  24844  xrge0gsumle  24868  iccpnfhmeo  24989  pcorev2  25074  pi1cpbl  25090  rrxmet  25455  ovoliunlem1  25550  voliunlem3  25600  uniioombllem2  25631  dyadss  25642  dvlipcn  26047  dv11cn  26054  dvle  26060  dvfsumge  26076  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem4  26084  dvfsum2  26089  idomrootle  26226  dgrsub  26326  vieta1lem2  26367  itgulm2  26466  radcnvlem1  26470  abelthlem7  26496  efcvx  26507  logdivlti  26676  logcnlem4  26701  logccv  26719  cxple2a  26755  cxpaddlelem  26808  cxpaddle  26809  leibpi  26999  scvxcvx  27043  amgmlem  27047  logdiflbnd  27052  lgamgulmlem2  27087  lgamgulmlem5  27090  lgambdd  27094  lgamcvg2  27112  ftalem2  27131  ppip1le  27218  ppieq0  27233  ppiltx  27234  chpeq0  27266  chtublem  27269  chtub  27270  logexprlim  27283  perfectlem2  27288  bposlem9  27350  2sqlem8  27484  chebbnd1lem1  27527  vmadivsum  27540  rplogsumlem1  27542  dchrisum0re  27571  dchrisum0lem1  27574  selberglem2  27604  chpdifbndlem1  27611  selberg3lem1  27615  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem6  27641  pntpbnd2  27645  pntibndlem2  27649  pntlemb  27655  pntlemr  27660  pntlemo  27665  ostth2lem2  27692  ostth2lem3  27693  nosupbnd2lem1  27774  noinfbnd2lem1  27789  mulsgt0  28184  tgcgrsub2  28617  legso  28621  krippenlem  28712  midex  28759  opphllem3  28771  trgcopy  28826  occllem  31331  nmcexi  32054  cnlnadjlem7  32101  hmopidmchi  32179  mgcf1o  32977  chnind  32984  chnlt  32986  chnso  32987  omndadd2d  33067  omndmul2  33071  omndmul3  33072  ogrpinv0le  33074  ogrpaddltbi  33077  ogrpaddltrbid  33079  ogrpinv0lt  33081  gsumle  33083  isarchi3  33176  archirngz  33178  archiabllem1b  33181  orngsqr  33313  ornglmulle  33314  orngrmulle  33315  isarchiofld  33326  esum2d  34073  omssubadd  34281  carsgclctun  34302  eulerpartlemgc  34343  dstfrvclim1  34458  fdvneggt  34593  fdvnegge  34595  logdivsqrle  34643  hgt750lemb  34649  subfaclim  35172  ovoliunnfl  37648  itg2addnclem3  37659  ftc1anclem8  37686  cntotbnd  37782  rrnmet  37815  3atlem1  39465  3atlem2  39466  llncvrlpln2  39539  lplncvrlvol2  39597  dalem25  39680  dalawlem7  39859  dalawlem11  39863  cdleme22g  40330  cdlemg18b  40661  cdlemg46  40717  dia2dimlem3  41048  dihord2  41209  3lexlogpow5ineq2  42036  3lexlogpow2ineq1  42039  3lexlogpow5ineq5  42041  aks4d1p1p7  42055  aks4d1p1  42057  aks4d1p6  42062  aks6d1c2lem4  42108  sticksstones6  42132  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  jm2.24nn  42947  jm2.27a  42993  amgm2d  44187  amgm3d  44188  amgm4d  44189  binomcxplemrat  44345  binomcxplemnotnn0  44351  monoord2xrv  45433  ioossioobi  45469  ioodvbdlimc2lem  45889  stoweidlem10  45965  stoweidlem11  45966  stoweidlem13  45968  stoweidlem14  45969  stoweidlem28  45983  stirlinglem11  46039  stirlinglem12  46040  dirkercncflem4  46061  fourierdlem4  46066  fourierdlem6  46068  fourierdlem11  46073  fourierdlem42  46104  fourierdlem51  46112  fourierdlem73  46134  fourierdlem79  46140  2pwp1prm  47513  perfectALTVlem2  47646  fllogbd  48409  nnpw2blen  48429  amgmwlem  49032  amgmlemALT  49033  amgmw2d  49034  young2d  49035