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

Theorem 3brtr3d 5137
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 5119 . 2 (𝜑 → (𝐴𝑅𝐵𝐶𝑅𝐷))
51, 4mpbid 231 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107
This theorem is referenced by:  ofrval  7630  difsnen  8998  domunsncan  9017  phplem2OLD  9163  infdifsn  9594  ltaddnq  10911  lemul2a  12011  mul2lt0rlt0  13018  xleadd2a  13174  xlemul2a  13209  monoord2  13940  expubnd  14083  bernneq2  14134  hashfun  14338  01sqrexlem2  15129  abs2dif2  15219  rlimdiv  15531  isercolllem1  15550  iseraltlem2  15568  iseraltlem3  15569  fsum00  15684  seqabs  15700  cvgcmp  15702  mertenslem1  15770  fprodle  15880  eftlub  15992  eirrlem  16087  bitscmp  16319  prmreclem1  16789  invisoinvl  17674  efgcpbl2  19540  pgpfaclem2  19862  unitgrp  20097  xblss2  23758  xmstri2  23822  mstri2  23823  xmstri  23824  mstri  23825  xmstri3  23826  mstri3  23827  msrtri  23828  nrmmetd  23933  nmtri  23985  nmoi2  24097  xrsxmet  24175  xrge0gsumle  24199  iccpnfhmeo  24311  pcorev2  24394  pi1cpbl  24410  rrxmet  24775  ovoliunlem1  24869  voliunlem3  24919  uniioombllem2  24950  dyadss  24961  dvlipcn  25361  dv11cn  25368  dvle  25374  dvfsumge  25389  dvfsumlem2  25394  dvfsumlem4  25396  dvfsum2  25401  dgrsub  25636  vieta1lem2  25674  itgulm2  25771  radcnvlem1  25775  abelthlem7  25800  efcvx  25811  logdivlti  25978  logcnlem4  26003  logccv  26021  cxple2a  26057  cxpaddlelem  26107  cxpaddle  26108  leibpi  26295  scvxcvx  26338  amgmlem  26342  logdiflbnd  26347  lgamgulmlem2  26382  lgamgulmlem5  26385  lgambdd  26389  lgamcvg2  26407  ftalem2  26426  ppip1le  26513  ppieq0  26528  ppiltx  26529  chpeq0  26559  chtublem  26562  chtub  26563  logexprlim  26576  perfectlem2  26581  bposlem9  26643  2sqlem8  26777  chebbnd1lem1  26820  vmadivsum  26833  rplogsumlem1  26835  dchrisum0re  26864  dchrisum0lem1  26867  selberglem2  26897  chpdifbndlem1  26904  selberg3lem1  26908  pntrlog2bndlem2  26929  pntrlog2bndlem3  26930  pntrlog2bndlem6  26934  pntpbnd2  26938  pntibndlem2  26942  pntlemb  26948  pntlemr  26953  pntlemo  26958  ostth2lem2  26985  ostth2lem3  26986  nosupbnd2lem1  27066  noinfbnd2lem1  27081  tgcgrsub2  27540  legso  27544  krippenlem  27635  midex  27682  opphllem3  27694  trgcopy  27749  occllem  30248  nmcexi  30971  cnlnadjlem7  31018  hmopidmchi  31096  mgcf1o  31866  omndadd2d  31919  omndmul2  31923  omndmul3  31924  ogrpinv0le  31926  ogrpaddltbi  31929  ogrpaddltrbid  31931  ogrpinv0lt  31933  gsumle  31935  isarchi3  32026  archirngz  32028  archiabllem1b  32031  orngsqr  32102  ornglmulle  32103  orngrmulle  32104  isarchiofld  32115  esum2d  32695  omssubadd  32903  carsgclctun  32924  eulerpartlemgc  32965  dstfrvclim1  33080  fdvneggt  33216  fdvnegge  33218  logdivsqrle  33266  hgt750lemb  33272  subfaclim  33785  ovoliunnfl  36123  itg2addnclem3  36134  ftc1anclem8  36161  cntotbnd  36258  rrnmet  36291  3atlem1  37949  3atlem2  37950  llncvrlpln2  38023  lplncvrlvol2  38081  dalem25  38164  dalawlem7  38343  dalawlem11  38347  cdleme22g  38814  cdlemg18b  39145  cdlemg46  39201  dia2dimlem3  39532  dihord2  39693  3lexlogpow5ineq2  40515  3lexlogpow2ineq1  40518  3lexlogpow5ineq5  40520  aks4d1p1p7  40534  aks4d1p1  40536  aks4d1p6  40541  sticksstones6  40562  jm2.24nn  41286  jm2.27a  41332  idomrootle  41525  amgm2d  42478  amgm3d  42479  amgm4d  42480  binomcxplemrat  42637  binomcxplemnotnn0  42643  monoord2xrv  43726  ioossioobi  43762  ioodvbdlimc2lem  44182  stoweidlem10  44258  stoweidlem11  44259  stoweidlem13  44261  stoweidlem14  44262  stoweidlem28  44276  stirlinglem11  44332  stirlinglem12  44333  dirkercncflem4  44354  fourierdlem4  44359  fourierdlem6  44361  fourierdlem11  44366  fourierdlem42  44397  fourierdlem51  44405  fourierdlem73  44427  fourierdlem79  44433  2pwp1prm  45788  perfectALTVlem2  45921  fllogbd  46653  nnpw2blen  46673  amgmwlem  47256  amgmlemALT  47257  amgmw2d  47258  young2d  47259
  Copyright terms: Public domain W3C validator