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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  ofrval  7732  difsnen  9109  domunsncan  9127  infdifsn  9688  ltaddnq  11089  lemul2a  12202  mul2lt0rlt0  13254  xleadd2a  13414  xlemul2a  13449  monoord2  14206  expubnd  14351  bernneq2  14404  hashfun  14612  01sqrexlem2  15442  abs2dif2  15533  rlimdiv  15845  isercolllem1  15864  iseraltlem2  15882  iseraltlem3  15883  fsum00  15997  seqabs  16013  cvgcmp  16015  mertenslem1  16085  fprodle  16195  eftlub  16309  eirrlem  16404  bitscmp  16640  prmreclem1  17126  invisoinvl  17997  chnind  18827  chnlt  18829  chnso  18830  ex-chn1  18843  efgcpbl2  20004  pgpfaclem2  20331  omndadd2d  20377  omndmul2  20380  omndmul3  20381  ogrpinv0le  20383  ogrpaddltbi  20386  ogrpaddltrbid  20388  ogrpinv0lt  20390  gsumle  20392  unitgrp  20646  orngsqr  21156  ornglmulle  21157  orngrmulle  21158  xblss2  24754  xmstri2  24818  mstri2  24819  xmstri  24820  mstri  24821  xmstri3  24822  mstri3  24823  msrtri  24824  nrmmetd  24926  nmtri  24978  nmoi2  25082  xrsxmet  25162  xrge0gsumle  25186  iccpnfhmeo  25299  pcorev2  25382  pi1cpbl  25398  rrxmet  25762  ovoliunlem1  25856  voliunlem3  25906  uniioombllem2  25937  dyadss  25948  dvlipcn  26347  dv11cn  26354  dvle  26360  dvfsumge  26375  dvfsumlem2  26380  dvfsumlem4  26382  dvfsum2  26387  idomrootle  26524  dgrsub  26624  vieta1lem2  26667  itgulm2  26769  radcnvlem1  26773  abelthlem7  26798  efcvx  26809  logdivlti  26981  logcnlem4  27006  logccv  27024  cxple2a  27060  cxpaddlelem  27112  cxpaddle  27113  leibpi  27303  scvxcvx  27346  amgmlem  27350  logdiflbnd  27355  lgamgulmlem2  27390  lgamgulmlem5  27393  lgambdd  27397  lgamcvg2  27415  ftalem2  27434  ppip1le  27521  ppieq0  27536  ppiltx  27537  chpeq0  27568  chtublem  27571  chtub  27572  logexprlim  27585  perfectlem2  27590  bposlem9  27652  2sqlem8  27786  chebbnd1lem1  27829  vmadivsum  27842  rplogsumlem1  27844  dchrisum0re  27873  dchrisum0lem1  27876  selberglem2  27906  chpdifbndlem1  27913  selberg3lem1  27917  pntrlog2bndlem2  27938  pntrlog2bndlem3  27939  pntrlog2bndlem6  27943  pntpbnd2  27947  pntibndlem2  27951  pntlemb  27957  pntlemr  27962  pntlemo  27967  ostth2lem2  27994  ostth2lem3  27995  nosupbnd2lem1  28105  noinfbnd2lem1  28120  mulsgt0  28563  bdayfinbndlem1  28886  tgcgrsub2  29091  legso  29095  krippenlem  29195  midex  29246  opphllem3  29258  trgcopy  29344  perpeqlem  29380  cgraer  29410  cgrabasimass  29411  occllem  31938  nmcexi  32661  cnlnadjlem7  32708  hmopidmchi  32786  oexpled  33500  mgcf1o  33640  isarchi3  33824  archirngz  33826  archiabllem1b  33829  isarchiofld  33836  cos9thpiminplylem1  34497  esum2d  34808  omssubadd  35015  carsgclctun  35036  eulerpartlemgc  35077  dstfrvclim1  35193  fdvneggt  35312  fdvnegge  35314  logdivsqrle  35362  hgt750lemb  35368  subfaclim  36133  ovoliunnfl  38785  itg2addnclem3  38796  ftc1anclem8  38823  cntotbnd  38933  rrnmet  38966  3atlem1  40743  3atlem2  40744  llncvrlpln2  40817  lplncvrlvol2  40875  dalem25  40958  dalawlem7  41137  dalawlem11  41141  cdleme22g  41608  cdlemg18b  41939  cdlemg46  41995  dia2dimlem3  42326  dihord2  42487  3lexlogpow5ineq2  43308  3lexlogpow2ineq1  43311  3lexlogpow5ineq5  43313  aks4d1p1p7  43327  aks4d1p1  43329  aks4d1p6  43334  aks6d1c2lem4  43380  sticksstones6  43404  bcled  43431  bcle2d  43432  aks6d1c7lem1  43433  jm2.24nn  44170  jm2.27a  44216  amgm2d  45401  amgm3d  45402  amgm4d  45403  binomcxplemrat  45537  binomcxplemnotnn0  45543  monoord2xrv  46708  ioossioobi  46744  ioodvbdlimc2lem  47159  stoweidlem10  47235  stoweidlem11  47236  stoweidlem13  47238  stoweidlem14  47239  stoweidlem28  47253  stirlinglem11  47309  stirlinglem12  47310  dirkercncflem4  47331  fourierdlem4  47336  fourierdlem6  47338  fourierdlem11  47343  fourierdlem42  47374  fourierdlem51  47382  fourierdlem73  47404  fourierdlem79  47410  chnerlem2  48108  2pwp1prm  48889  perfectALTVlem2  49035  fllogbd  49887  nnpw2blen  49907  funcoppc4  50475  amgmwlem  51299  amgmlemALT  51300  amgmw2d  51301  young2d  51302