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

Theorem 3brtr3d 4675
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 4657 . 2 (𝜑 → (𝐴𝑅𝐵𝐶𝑅𝐷))
51, 4mpbid 222 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481   class class class wbr 4644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645
This theorem is referenced by:  ofrval  6892  difsnen  8027  domunsncan  8045  phplem2  8125  infdifsn  8539  ltaddnq  9781  lemul2a  10863  mul2lt0rlt0  11917  xleadd2a  12069  xlemul2a  12104  monoord2  12815  expubnd  12904  bernneq2  12974  hashfun  13207  sqrlem2  13965  abs2dif2  14054  rlimdiv  14357  isercolllem1  14376  iseraltlem2  14394  iseraltlem3  14395  fsum00  14511  seqabs  14527  cvgcmp  14529  mertenslem1  14597  eftlub  14820  eirrlem  14913  bitscmp  15141  prmreclem1  15601  invisoinvl  16431  efgcpbl2  18151  pgpfaclem2  18462  unitgrp  18648  xblss2  22188  xmstri2  22252  mstri2  22253  xmstri  22254  mstri  22255  xmstri3  22256  mstri3  22257  msrtri  22258  nrmmetd  22360  nmtri  22411  nmoi2  22515  xrsxmet  22593  xrge0gsumle  22617  iccpnfhmeo  22725  pcorev2  22809  pi1cpbl  22825  rrxmet  23172  ovoliunlem1  23251  voliunlem3  23301  uniioombllem2  23332  dyadss  23343  dvlipcn  23738  dv11cn  23745  dvle  23751  dvfsumge  23766  dvfsumlem2  23771  dvfsumlem4  23773  dvfsum2  23778  dgrsub  24009  vieta1lem2  24047  itgulm2  24144  radcnvlem1  24148  abelthlem7  24173  efcvx  24184  logdivlti  24347  logcnlem4  24372  logccv  24390  cxple2a  24426  cxpaddlelem  24473  cxpaddle  24474  leibpi  24650  scvxcvx  24693  amgmlem  24697  logdiflbnd  24702  lgamgulmlem2  24737  lgamgulmlem5  24740  lgambdd  24744  lgamcvg2  24762  ftalem2  24781  ppip1le  24868  ppieq0  24883  ppiltx  24884  chpeq0  24914  chtublem  24917  chtub  24918  logexprlim  24931  perfectlem2  24936  bposlem9  24998  2sqlem8  25132  chebbnd1lem1  25139  vmadivsum  25152  rplogsumlem1  25154  dchrisum0re  25183  dchrisum0lem1  25186  selberglem2  25216  chpdifbndlem1  25223  selberg3lem1  25227  pntrlog2bndlem2  25248  pntrlog2bndlem3  25249  pntrlog2bndlem6  25253  pntpbnd2  25257  pntibndlem2  25261  pntlemb  25267  pntlemr  25272  pntlemo  25277  ostth2lem2  25304  ostth2lem3  25305  tgcgrsub2  25471  legso  25475  krippenlem  25566  midex  25610  opphllem3  25622  trgcopy  25677  occllem  28132  nmcexi  28855  cnlnadjlem7  28902  hmopidmchi  28980  omndadd2d  29682  omndmul2  29686  omndmul3  29687  ogrpinvOLD  29689  ogrpinv0le  29690  ogrpaddltbi  29693  ogrpaddltrbid  29695  ogrpinv0lt  29697  isarchi3  29715  archirngz  29717  archiabllem1b  29720  gsumle  29753  orngsqr  29778  ornglmulle  29779  orngrmulle  29780  isarchiofld  29791  esum2d  30129  omssubadd  30336  carsgclctun  30357  eulerpartlemgc  30398  dstfrvclim1  30513  fdvneggt  30652  fdvnegge  30654  logdivsqrle  30702  hgt750lemb  30708  subfaclim  31144  nosupbnd2lem1  31835  ovoliunnfl  33422  itg2addnclem3  33434  ftc1anclem8  33463  cntotbnd  33566  rrnmet  33599  3atlem1  34588  3atlem2  34589  llncvrlpln2  34662  lplncvrlvol2  34720  dalem25  34803  dalawlem7  34982  dalawlem11  34986  cdleme22g  35455  cdlemg18b  35786  cdlemg46  35842  dia2dimlem3  36174  dihord2  36335  jm2.24nn  37345  jm2.27a  37391  idomrootle  37592  amgm2d  38321  amgm3d  38322  amgm4d  38323  binomcxplemrat  38369  binomcxplemnotnn0  38375  ioossioobi  39546  ioodvbdlimc2lem  39912  stoweidlem10  39990  stoweidlem11  39991  stoweidlem13  39993  stoweidlem14  39994  stoweidlem28  40008  stirlinglem11  40064  stirlinglem12  40065  dirkercncflem4  40086  fourierdlem4  40091  fourierdlem6  40093  fourierdlem11  40098  fourierdlem42  40129  fourierdlem51  40137  fourierdlem73  40159  fourierdlem79  40165  2pwp1prm  41268  perfectALTVlem2  41396  fllogbd  42119  nnpw2blen  42139  amgmwlem  42313  amgmlemALT  42314  amgmw2d  42315  young2d  42316
  Copyright terms: Public domain W3C validator