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

Theorem 3brtr3d 4840
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 4822 . 2 (𝜑 → (𝐴𝑅𝐵𝐶𝑅𝐷))
51, 4mpbid 223 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652   class class class wbr 4809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-br 4810
This theorem is referenced by:  ofrval  7105  difsnen  8249  domunsncan  8267  phplem2  8347  infdifsn  8769  ltaddnq  10049  lemul2a  11132  mul2lt0rlt0  12130  xleadd2a  12286  xlemul2a  12321  monoord2  13039  expubnd  13128  bernneq2  13198  hashfun  13425  sqrlem2  14269  abs2dif2  14358  rlimdiv  14661  isercolllem1  14680  iseraltlem2  14698  iseraltlem3  14699  fsum00  14814  seqabs  14830  cvgcmp  14832  mertenslem1  14899  eftlub  15121  eirrlem  15214  bitscmp  15441  prmreclem1  15899  invisoinvl  16715  efgcpbl2  18436  pgpfaclem2  18748  unitgrp  18934  xblss2  22486  xmstri2  22550  mstri2  22551  xmstri  22552  mstri  22553  xmstri3  22554  mstri3  22555  msrtri  22556  nrmmetd  22658  nmtri  22709  nmoi2  22813  xrsxmet  22891  xrge0gsumle  22915  iccpnfhmeo  23023  pcorev2  23106  pi1cpbl  23122  rrxmet  23480  ovoliunlem1  23560  voliunlem3  23610  uniioombllem2  23641  dyadss  23652  dvlipcn  24048  dv11cn  24055  dvle  24061  dvfsumge  24076  dvfsumlem2  24081  dvfsumlem4  24083  dvfsum2  24088  dgrsub  24319  vieta1lem2  24357  itgulm2  24454  radcnvlem1  24458  abelthlem7  24483  efcvx  24494  logdivlti  24657  logcnlem4  24682  logccv  24700  cxple2a  24736  cxpaddlelem  24783  cxpaddle  24784  leibpi  24960  scvxcvx  25003  amgmlem  25007  logdiflbnd  25012  lgamgulmlem2  25047  lgamgulmlem5  25050  lgambdd  25054  lgamcvg2  25072  ftalem2  25091  ppip1le  25178  ppieq0  25193  ppiltx  25194  chpeq0  25224  chtublem  25227  chtub  25228  logexprlim  25241  perfectlem2  25246  bposlem9  25308  2sqlem8  25442  chebbnd1lem1  25449  vmadivsum  25462  rplogsumlem1  25464  dchrisum0re  25493  dchrisum0lem1  25496  selberglem2  25526  chpdifbndlem1  25533  selberg3lem1  25537  pntrlog2bndlem2  25558  pntrlog2bndlem3  25559  pntrlog2bndlem6  25563  pntpbnd2  25567  pntibndlem2  25571  pntlemb  25577  pntlemr  25582  pntlemo  25587  ostth2lem2  25614  ostth2lem3  25615  tgcgrsub2  25781  legso  25785  krippenlem  25876  midex  25920  opphllem3  25932  trgcopy  25987  occllem  28618  nmcexi  29341  cnlnadjlem7  29388  hmopidmchi  29466  omndadd2d  30155  omndmul2  30159  omndmul3  30160  ogrpinvOLD  30162  ogrpinv0le  30163  ogrpaddltbi  30166  ogrpaddltrbid  30168  ogrpinv0lt  30170  isarchi3  30188  archirngz  30190  archiabllem1b  30193  gsumle  30226  orngsqr  30251  ornglmulle  30252  orngrmulle  30253  isarchiofld  30264  esum2d  30602  omssubadd  30809  carsgclctun  30830  eulerpartlemgc  30871  dstfrvclim1  30987  fdvneggt  31129  fdvnegge  31131  logdivsqrle  31179  hgt750lemb  31185  subfaclim  31618  nosupbnd2lem1  32305  ovoliunnfl  33875  itg2addnclem3  33886  ftc1anclem8  33915  cntotbnd  34017  rrnmet  34050  3atlem1  35439  3atlem2  35440  llncvrlpln2  35513  lplncvrlvol2  35571  dalem25  35654  dalawlem7  35833  dalawlem11  35837  cdleme22g  36304  cdlemg18b  36635  cdlemg46  36691  dia2dimlem3  37022  dihord2  37183  jm2.24nn  38203  jm2.27a  38249  idomrootle  38450  amgm2d  39175  amgm3d  39176  amgm4d  39177  binomcxplemrat  39223  binomcxplemnotnn0  39229  monoord2xrv  40351  ioossioobi  40382  ioodvbdlimc2lem  40787  stoweidlem10  40864  stoweidlem11  40865  stoweidlem13  40867  stoweidlem14  40868  stoweidlem28  40882  stirlinglem11  40938  stirlinglem12  40939  dirkercncflem4  40960  fourierdlem4  40965  fourierdlem6  40967  fourierdlem11  40972  fourierdlem42  41003  fourierdlem51  41011  fourierdlem73  41033  fourierdlem79  41039  2pwp1prm  42179  perfectALTVlem2  42307  fllogbd  43023  nnpw2blen  43043  amgmwlem  43220  amgmlemALT  43221  amgmw2d  43222  young2d  43223
  Copyright terms: Public domain W3C validator