Theorem 3brtr3d 5140

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  ofrval  7694  difsnen  9061  domunsncan  9079  infdifsn  9640  ltaddnq  10987  lemul2a  12098  mul2lt0rlt0  13150  xleadd2a  13310  xlemul2a  13345  monoord2  14101  expubnd  14246  bernneq2  14298  hashfun  14506  01sqrexlem2  15334  abs2dif2  15425  rlimdiv  15737  isercolllem1  15756  iseraltlem2  15774  iseraltlem3  15775  fsum00  15889  seqabs  15905  cvgcmp  15907  mertenslem1  15977  fprodle  16089  eftlub  16203  eirrlem  16298  bitscmp  16534  prmreclem1  17014  invisoinvl  17885  chnind  18715  chnlt  18717  chnso  18718  ex-chn1  18731  efgcpbl2  19890  pgpfaclem2  20217  omndadd2d  20263  omndmul2  20266  omndmul3  20267  ogrpinv0le  20269  ogrpaddltbi  20272  ogrpaddltrbid  20274  ogrpinv0lt  20276  gsumle  20278  unitgrp  20530  orngsqr  21038  ornglmulle  21039  orngrmulle  21040  xblss2  24634  xmstri2  24698  mstri2  24699  xmstri  24700  mstri  24701  xmstri3  24702  mstri3  24703  msrtri  24704  nrmmetd  24806  nmtri  24858  nmoi2  24962  xrsxmet  25042  xrge0gsumle  25066  iccpnfhmeo  25179  pcorev2  25262  pi1cpbl  25278  rrxmet  25642  ovoliunlem1  25736  voliunlem3  25786  uniioombllem2  25817  dyadss  25828  dvlipcn  26228  dv11cn  26235  dvle  26241  dvfsumge  26256  dvfsumlem2  26261  dvfsumlem4  26263  dvfsum2  26268  idomrootle  26405  dgrsub  26505  vieta1lem2  26550  itgulm2  26652  radcnvlem1  26656  abelthlem7  26681  efcvx  26692  logdivlti  26865  logcnlem4  26890  logccv  26908  cxple2a  26944  cxpaddlelem  26996  cxpaddle  26997  leibpi  27187  scvxcvx  27230  amgmlem  27234  logdiflbnd  27239  lgamgulmlem2  27274  lgamgulmlem5  27277  lgambdd  27281  lgamcvg2  27299  ftalem2  27318  ppip1le  27405  ppieq0  27420  ppiltx  27421  chpeq0  27452  chtublem  27455  chtub  27456  logexprlim  27469  perfectlem2  27474  bposlem9  27536  2sqlem8  27670  chebbnd1lem1  27713  vmadivsum  27726  rplogsumlem1  27728  dchrisum0re  27757  dchrisum0lem1  27760  selberglem2  27790  chpdifbndlem1  27797  selberg3lem1  27801  pntrlog2bndlem2  27822  pntrlog2bndlem3  27823  pntrlog2bndlem6  27827  pntpbnd2  27831  pntibndlem2  27835  pntlemb  27841  pntlemr  27846  pntlemo  27851  ostth2lem2  27878  ostth2lem3  27879  nosupbnd2lem1  27959  noinfbnd2lem1  27974  mulsgt0  28417  bdayfinbndlem1  28740  tgcgrsub2  28945  legso  28949  krippenlem  29049  midex  29100  opphllem3  29112  trgcopy  29198  perpeqlem  29234  cgraer  29264  cgrabasimass  29265  occllem  31792  nmcexi  32515  cnlnadjlem7  32562  hmopidmchi  32640  oexpled  33314  mgcf1o  33451  isarchi3  33635  archirngz  33637  archiabllem1b  33640  isarchiofld  33647  cos9thpiminplylem1  34300  esum2d  34611  omssubadd  34819  carsgclctun  34840  eulerpartlemgc  34881  dstfrvclim1  34997  fdvneggt  35116  fdvnegge  35118  logdivsqrle  35166  hgt750lemb  35172  subfaclim  35775  ovoliunnfl  38419  itg2addnclem3  38430  ftc1anclem8  38457  cntotbnd  38554  rrnmet  38587  3atlem1  40364  3atlem2  40365  llncvrlpln2  40438  lplncvrlvol2  40496  dalem25  40579  dalawlem7  40758  dalawlem11  40762  cdleme22g  41229  cdlemg18b  41560  cdlemg46  41616  dia2dimlem3  41947  dihord2  42108  3lexlogpow5ineq2  42929  3lexlogpow2ineq1  42932  3lexlogpow5ineq5  42934  aks4d1p1p7  42948  aks4d1p1  42950  aks4d1p6  42955  aks6d1c2lem4  43001  sticksstones6  43025  bcled  43052  bcle2d  43053  aks6d1c7lem1  43054  jm2.24nn  43808  jm2.27a  43854  amgm2d  45046  amgm3d  45047  amgm4d  45048  binomcxplemrat  45182  binomcxplemnotnn0  45188  monoord2xrv  46319  ioossioobi  46355  ioodvbdlimc2lem  46770  stoweidlem10  46846  stoweidlem11  46847  stoweidlem13  46849  stoweidlem14  46850  stoweidlem28  46864  stirlinglem11  46920  stirlinglem12  46921  dirkercncflem4  46942  fourierdlem4  46947  fourierdlem6  46949  fourierdlem11  46954  fourierdlem42  46985  fourierdlem51  46993  fourierdlem73  47015  fourierdlem79  47021  chnerlem2  47719  2pwp1prm  48500  perfectALTVlem2  48646  fllogbd  49498  nnpw2blen  49518  funcoppc4  50078  amgmwlem  50828  amgmlemALT  50829  amgmw2d  50830  young2d  50831