Theorem 3brtr3d 5097

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  ofrval  7419  difsnen  8599  domunsncan  8617  phplem2  8697  infdifsn  9120  ltaddnq  10396  lemul2a  11495  mul2lt0rlt0  12492  xleadd2a  12648  xlemul2a  12683  monoord2  13402  expubnd  13542  bernneq2  13592  hashfun  13799  sqrlem2  14603  abs2dif2  14693  rlimdiv  15002  isercolllem1  15021  iseraltlem2  15039  iseraltlem3  15040  fsum00  15153  seqabs  15169  cvgcmp  15171  mertenslem1  15240  fprodle  15350  eftlub  15462  eirrlem  15557  bitscmp  15787  prmreclem1  16252  invisoinvl  17060  efgcpbl2  18883  pgpfaclem2  19204  unitgrp  19417  xblss2  23012  xmstri2  23076  mstri2  23077  xmstri  23078  mstri  23079  xmstri3  23080  mstri3  23081  msrtri  23082  nrmmetd  23184  nmtri  23235  nmoi2  23339  xrsxmet  23417  xrge0gsumle  23441  iccpnfhmeo  23549  pcorev2  23632  pi1cpbl  23648  rrxmet  24011  ovoliunlem1  24103  voliunlem3  24153  uniioombllem2  24184  dyadss  24195  dvlipcn  24591  dv11cn  24598  dvle  24604  dvfsumge  24619  dvfsumlem2  24624  dvfsumlem4  24626  dvfsum2  24631  dgrsub  24862  vieta1lem2  24900  itgulm2  24997  radcnvlem1  25001  abelthlem7  25026  efcvx  25037  logdivlti  25203  logcnlem4  25228  logccv  25246  cxple2a  25282  cxpaddlelem  25332  cxpaddle  25333  leibpi  25520  scvxcvx  25563  amgmlem  25567  logdiflbnd  25572  lgamgulmlem2  25607  lgamgulmlem5  25610  lgambdd  25614  lgamcvg2  25632  ftalem2  25651  ppip1le  25738  ppieq0  25753  ppiltx  25754  chpeq0  25784  chtublem  25787  chtub  25788  logexprlim  25801  perfectlem2  25806  bposlem9  25868  2sqlem8  26002  chebbnd1lem1  26045  vmadivsum  26058  rplogsumlem1  26060  dchrisum0re  26089  dchrisum0lem1  26092  selberglem2  26122  chpdifbndlem1  26129  selberg3lem1  26133  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem6  26159  pntpbnd2  26163  pntibndlem2  26167  pntlemb  26173  pntlemr  26178  pntlemo  26183  ostth2lem2  26210  ostth2lem3  26211  tgcgrsub2  26381  legso  26385  krippenlem  26476  midex  26523  opphllem3  26535  trgcopy  26590  occllem  29080  nmcexi  29803  cnlnadjlem7  29850  hmopidmchi  29928  omndadd2d  30709  omndmul2  30713  omndmul3  30714  ogrpinv0le  30716  ogrpaddltbi  30719  ogrpaddltrbid  30721  ogrpinv0lt  30723  gsumle  30725  isarchi3  30816  archirngz  30818  archiabllem1b  30821  orngsqr  30877  ornglmulle  30878  orngrmulle  30879  isarchiofld  30890  esum2d  31352  omssubadd  31558  carsgclctun  31579  eulerpartlemgc  31620  dstfrvclim1  31735  fdvneggt  31871  fdvnegge  31873  logdivsqrle  31921  hgt750lemb  31927  subfaclim  32435  nosupbnd2lem1  33215  ovoliunnfl  34949  itg2addnclem3  34960  ftc1anclem8  34989  cntotbnd  35089  rrnmet  35122  3atlem1  36634  3atlem2  36635  llncvrlpln2  36708  lplncvrlvol2  36766  dalem25  36849  dalawlem7  37028  dalawlem11  37032  cdleme22g  37499  cdlemg18b  37830  cdlemg46  37886  dia2dimlem3  38217  dihord2  38378  jm2.24nn  39605  jm2.27a  39651  idomrootle  39844  amgm2d  40600  amgm3d  40601  amgm4d  40602  binomcxplemrat  40731  binomcxplemnotnn0  40737  monoord2xrv  41809  ioossioobi  41842  ioodvbdlimc2lem  42268  stoweidlem10  42344  stoweidlem11  42345  stoweidlem13  42347  stoweidlem14  42348  stoweidlem28  42362  stirlinglem11  42418  stirlinglem12  42419  dirkercncflem4  42440  fourierdlem4  42445  fourierdlem6  42447  fourierdlem11  42452  fourierdlem42  42483  fourierdlem51  42491  fourierdlem73  42513  fourierdlem79  42519  2pwp1prm  43800  perfectALTVlem2  43936  fllogbd  44669  nnpw2blen  44689  amgmwlem  44952  amgmlemALT  44953  amgmw2d  44954  young2d  44955