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

Theorem 3brtr3d 5096
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 5078 . 2 (𝜑 → (𝐴𝑅𝐵𝐶𝑅𝐷))
51, 4mpbid 234 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533   class class class wbr 5065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-br 5066
This theorem is referenced by:  ofrval  7418  difsnen  8598  domunsncan  8616  phplem2  8696  infdifsn  9119  ltaddnq  10395  lemul2a  11494  mul2lt0rlt0  12490  xleadd2a  12646  xlemul2a  12681  monoord2  13400  expubnd  13540  bernneq2  13590  hashfun  13797  sqrlem2  14602  abs2dif2  14692  rlimdiv  15001  isercolllem1  15020  iseraltlem2  15038  iseraltlem3  15039  fsum00  15152  seqabs  15168  cvgcmp  15170  mertenslem1  15239  fprodle  15349  eftlub  15461  eirrlem  15556  bitscmp  15786  prmreclem1  16251  invisoinvl  17059  efgcpbl2  18882  pgpfaclem2  19203  unitgrp  19416  xblss2  23011  xmstri2  23075  mstri2  23076  xmstri  23077  mstri  23078  xmstri3  23079  mstri3  23080  msrtri  23081  nrmmetd  23183  nmtri  23234  nmoi2  23338  xrsxmet  23416  xrge0gsumle  23440  iccpnfhmeo  23548  pcorev2  23631  pi1cpbl  23647  rrxmet  24010  ovoliunlem1  24102  voliunlem3  24152  uniioombllem2  24183  dyadss  24194  dvlipcn  24590  dv11cn  24597  dvle  24603  dvfsumge  24618  dvfsumlem2  24623  dvfsumlem4  24625  dvfsum2  24630  dgrsub  24861  vieta1lem2  24899  itgulm2  24996  radcnvlem1  25000  abelthlem7  25025  efcvx  25036  logdivlti  25202  logcnlem4  25227  logccv  25245  cxple2a  25281  cxpaddlelem  25331  cxpaddle  25332  leibpi  25519  scvxcvx  25562  amgmlem  25566  logdiflbnd  25571  lgamgulmlem2  25606  lgamgulmlem5  25609  lgambdd  25613  lgamcvg2  25631  ftalem2  25650  ppip1le  25737  ppieq0  25752  ppiltx  25753  chpeq0  25783  chtublem  25786  chtub  25787  logexprlim  25800  perfectlem2  25805  bposlem9  25867  2sqlem8  26001  chebbnd1lem1  26044  vmadivsum  26057  rplogsumlem1  26059  dchrisum0re  26088  dchrisum0lem1  26091  selberglem2  26121  chpdifbndlem1  26128  selberg3lem1  26132  pntrlog2bndlem2  26153  pntrlog2bndlem3  26154  pntrlog2bndlem6  26158  pntpbnd2  26162  pntibndlem2  26166  pntlemb  26172  pntlemr  26177  pntlemo  26182  ostth2lem2  26209  ostth2lem3  26210  tgcgrsub2  26380  legso  26384  krippenlem  26475  midex  26522  opphllem3  26534  trgcopy  26589  occllem  29079  nmcexi  29802  cnlnadjlem7  29849  hmopidmchi  29927  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  34933  itg2addnclem3  34944  ftc1anclem8  34973  cntotbnd  35073  rrnmet  35106  3atlem1  36618  3atlem2  36619  llncvrlpln2  36692  lplncvrlvol2  36750  dalem25  36833  dalawlem7  37012  dalawlem11  37016  cdleme22g  37483  cdlemg18b  37814  cdlemg46  37870  dia2dimlem3  38201  dihord2  38362  jm2.24nn  39556  jm2.27a  39602  idomrootle  39795  amgm2d  40551  amgm3d  40552  amgm4d  40553  binomcxplemrat  40682  binomcxplemnotnn0  40688  monoord2xrv  41760  ioossioobi  41793  ioodvbdlimc2lem  42219  stoweidlem10  42296  stoweidlem11  42297  stoweidlem13  42299  stoweidlem14  42300  stoweidlem28  42314  stirlinglem11  42370  stirlinglem12  42371  dirkercncflem4  42392  fourierdlem4  42397  fourierdlem6  42399  fourierdlem11  42404  fourierdlem42  42435  fourierdlem51  42443  fourierdlem73  42465  fourierdlem79  42471  2pwp1prm  43752  perfectALTVlem2  43888  fllogbd  44621  nnpw2blen  44641  amgmwlem  44904  amgmlemALT  44905  amgmw2d  44906  young2d  44907
  Copyright terms: Public domain W3C validator