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

Theorem 3brtr3d 4608
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 4590 . 2 (𝜑 → (𝐴𝑅𝐵𝐶𝑅𝐷))
51, 4mpbid 220 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   class class class wbr 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578
This theorem is referenced by:  ofrval  6782  difsnen  7904  domunsncan  7922  phplem2  8002  infdifsn  8414  ltaddnq  9652  lemul2a  10727  mul2lt0rlt0  11764  xleadd2a  11913  xlemul2a  11948  monoord2  12649  expubnd  12738  bernneq2  12808  hashfun  13036  sqrlem2  13778  abs2dif2  13867  rlimdiv  14170  isercolllem1  14189  iseraltlem2  14207  iseraltlem3  14208  fsum00  14317  seqabs  14333  cvgcmp  14335  mertenslem1  14401  eftlub  14624  eirrlem  14717  bitscmp  14944  prmreclem1  15404  invisoinvl  16219  efgcpbl2  17939  pgpfaclem2  18250  unitgrp  18436  xblss2  21958  xmstri2  22022  mstri2  22023  xmstri  22024  mstri  22025  xmstri3  22026  mstri3  22027  msrtri  22028  nrmmetd  22130  nmtri  22180  nmoi2  22276  xrsxmet  22352  xrge0gsumle  22376  iccpnfhmeo  22483  pcorev2  22567  pi1cpbl  22583  rrxmet  22916  ovoliunlem1  22994  voliunlem3  23044  uniioombllem2  23074  dyadss  23085  dvlipcn  23478  dv11cn  23485  dvle  23491  dvfsumge  23506  dvfsumlem2  23511  dvfsumlem4  23513  dvfsum2  23518  dgrsub  23749  vieta1lem2  23787  itgulm2  23884  radcnvlem1  23888  abelthlem7  23913  efcvx  23924  logdivlti  24087  logcnlem4  24108  logccv  24126  cxple2a  24162  cxpaddlelem  24209  cxpaddle  24210  leibpi  24386  scvxcvx  24429  amgmlem  24433  logdiflbnd  24438  lgamgulmlem2  24473  lgamgulmlem5  24476  lgambdd  24480  lgamcvg2  24498  ftalem2  24517  ppip1le  24604  ppieq0  24619  ppiltx  24620  chpeq0  24650  chtublem  24653  chtub  24654  logexprlim  24667  perfectlem2  24672  bposlem9  24734  2sqlem8  24868  chebbnd1lem1  24875  vmadivsum  24888  rplogsumlem1  24890  dchrisum0re  24919  dchrisum0lem1  24922  selberglem2  24952  chpdifbndlem1  24959  selberg3lem1  24963  pntrlog2bndlem2  24984  pntrlog2bndlem3  24985  pntrlog2bndlem6  24989  pntpbnd2  24993  pntibndlem2  24997  pntlemb  25003  pntlemr  25008  pntlemo  25013  ostth2lem2  25040  ostth2lem3  25041  tgcgrsub2  25208  legso  25212  krippenlem  25303  midex  25347  opphllem3  25359  trgcopy  25414  occllem  27352  nmcexi  28075  cnlnadjlem7  28122  hmopidmchi  28200  omndadd2d  28845  omndmul2  28849  omndmul3  28850  ogrpinvOLD  28852  ogrpinv0le  28853  ogrpaddltbi  28856  ogrpaddltrbid  28858  ogrpinv0lt  28860  isarchi3  28878  archirngz  28880  archiabllem1b  28883  gsumle  28916  orngsqr  28941  ornglmulle  28942  orngrmulle  28943  isarchiofld  28954  esum2d  29288  omssubadd  29495  carsgclctun  29516  eulerpartlemgc  29557  dstfrvclim1  29672  subfaclim  30230  ovoliunnfl  32417  itg2addnclem3  32429  ftc1anclem8  32458  cntotbnd  32561  rrnmet  32594  3atlem1  33583  3atlem2  33584  llncvrlpln2  33657  lplncvrlvol2  33715  dalem25  33798  dalawlem7  33977  dalawlem11  33981  cdleme22g  34450  cdlemg18b  34781  cdlemg46  34837  dia2dimlem3  35169  dihord2  35330  jm2.24nn  36340  jm2.27a  36386  idomrootle  36588  amgm2d  37319  amgm3d  37320  amgm4d  37321  binomcxplemrat  37367  binomcxplemnotnn0  37373  ioossioobi  38387  ioodvbdlimc2lem  38621  stoweidlem10  38700  stoweidlem11  38701  stoweidlem13  38703  stoweidlem14  38704  stoweidlem28  38718  stirlinglem11  38774  stirlinglem12  38775  dirkercncflem4  38796  fourierdlem4  38801  fourierdlem6  38803  fourierdlem11  38808  fourierdlem42  38839  fourierdlem51  38847  fourierdlem73  38869  fourierdlem79  38875  2pwp1prm  39839  perfectALTVlem2  39963  fllogbd  42147  nnpw2blen  42167  amgmwlem  42313  amgmlemALT  42314  amgmw2d  42315  young2d  42316
  Copyright terms: Public domain W3C validator