MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3brtr3d Structured version   Visualization version   GIF version

Theorem 3brtr3d 5089
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
StepHypRef Expression
1 3brtr3d.1 . 2 (𝜑𝐴𝑅𝐵)
2 3brtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
3 3brtr3d.3 . . 3 (𝜑𝐵 = 𝐷)
42, 3breq12d 5071 . 2 (𝜑 → (𝐴𝑅𝐵𝐶𝑅𝐷))
51, 4mpbid 233 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528   class class class wbr 5058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059
This theorem is referenced by:  ofrval  7408  difsnen  8588  domunsncan  8606  phplem2  8686  infdifsn  9109  ltaddnq  10385  lemul2a  11484  mul2lt0rlt0  12481  xleadd2a  12637  xlemul2a  12672  monoord2  13391  expubnd  13531  bernneq2  13581  hashfun  13788  sqrlem2  14593  abs2dif2  14683  rlimdiv  14992  isercolllem1  15011  iseraltlem2  15029  iseraltlem3  15030  fsum00  15143  seqabs  15159  cvgcmp  15161  mertenslem1  15230  fprodle  15340  eftlub  15452  eirrlem  15547  bitscmp  15777  prmreclem1  16242  invisoinvl  17050  efgcpbl2  18814  pgpfaclem2  19135  unitgrp  19348  xblss2  22941  xmstri2  23005  mstri2  23006  xmstri  23007  mstri  23008  xmstri3  23009  mstri3  23010  msrtri  23011  nrmmetd  23113  nmtri  23164  nmoi2  23268  xrsxmet  23346  xrge0gsumle  23370  iccpnfhmeo  23478  pcorev2  23561  pi1cpbl  23577  rrxmet  23940  ovoliunlem1  24032  voliunlem3  24082  uniioombllem2  24113  dyadss  24124  dvlipcn  24520  dv11cn  24527  dvle  24533  dvfsumge  24548  dvfsumlem2  24553  dvfsumlem4  24555  dvfsum2  24560  dgrsub  24791  vieta1lem2  24829  itgulm2  24926  radcnvlem1  24930  abelthlem7  24955  efcvx  24966  logdivlti  25130  logcnlem4  25155  logccv  25173  cxple2a  25209  cxpaddlelem  25259  cxpaddle  25260  leibpi  25448  scvxcvx  25491  amgmlem  25495  logdiflbnd  25500  lgamgulmlem2  25535  lgamgulmlem5  25538  lgambdd  25542  lgamcvg2  25560  ftalem2  25579  ppip1le  25666  ppieq0  25681  ppiltx  25682  chpeq0  25712  chtublem  25715  chtub  25716  logexprlim  25729  perfectlem2  25734  bposlem9  25796  2sqlem8  25930  chebbnd1lem1  25973  vmadivsum  25986  rplogsumlem1  25988  dchrisum0re  26017  dchrisum0lem1  26020  selberglem2  26050  chpdifbndlem1  26057  selberg3lem1  26061  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem6  26087  pntpbnd2  26091  pntibndlem2  26095  pntlemb  26101  pntlemr  26106  pntlemo  26111  ostth2lem2  26138  ostth2lem3  26139  tgcgrsub2  26309  legso  26313  krippenlem  26404  midex  26451  opphllem3  26463  trgcopy  26518  occllem  29008  nmcexi  29731  cnlnadjlem7  29778  hmopidmchi  29856  omndadd2d  30637  omndmul2  30641  omndmul3  30642  ogrpinv0le  30644  ogrpaddltbi  30647  ogrpaddltrbid  30649  ogrpinv0lt  30651  gsumle  30653  isarchi3  30744  archirngz  30746  archiabllem1b  30749  orngsqr  30805  ornglmulle  30806  orngrmulle  30807  isarchiofld  30818  esum2d  31252  omssubadd  31458  carsgclctun  31479  eulerpartlemgc  31520  dstfrvclim1  31635  fdvneggt  31771  fdvnegge  31773  logdivsqrle  31821  hgt750lemb  31827  subfaclim  32333  nosupbnd2lem1  33113  ovoliunnfl  34816  itg2addnclem3  34827  ftc1anclem8  34856  cntotbnd  34957  rrnmet  34990  3atlem1  36501  3atlem2  36502  llncvrlpln2  36575  lplncvrlvol2  36633  dalem25  36716  dalawlem7  36895  dalawlem11  36899  cdleme22g  37366  cdlemg18b  37697  cdlemg46  37753  dia2dimlem3  38084  dihord2  38245  jm2.24nn  39436  jm2.27a  39482  idomrootle  39675  amgm2d  40432  amgm3d  40433  amgm4d  40434  binomcxplemrat  40562  binomcxplemnotnn0  40568  monoord2xrv  41640  ioossioobi  41673  ioodvbdlimc2lem  42099  stoweidlem10  42176  stoweidlem11  42177  stoweidlem13  42179  stoweidlem14  42180  stoweidlem28  42194  stirlinglem11  42250  stirlinglem12  42251  dirkercncflem4  42272  fourierdlem4  42277  fourierdlem6  42279  fourierdlem11  42284  fourierdlem42  42315  fourierdlem51  42323  fourierdlem73  42345  fourierdlem79  42351  2pwp1prm  43598  perfectALTVlem2  43734  fllogbd  44518  nnpw2blen  44538  amgmwlem  44801  amgmlemALT  44802  amgmw2d  44803  young2d  44804
  Copyright terms: Public domain W3C validator