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

Theorem 3brtr3d 4068
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
3brtr3d.1  |-  ( ph  ->  A R B )
3brtr3d.2  |-  ( ph  ->  A  =  C )
3brtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3brtr3d  |-  ( ph  ->  C R D )

Proof of Theorem 3brtr3d
StepHypRef Expression
1 3brtr3d.1 . 2  |-  ( ph  ->  A R B )
2 3brtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
3 3brtr3d.3 . . 3  |-  ( ph  ->  B  =  D )
42, 3breq12d 4052 . 2  |-  ( ph  ->  ( A R B  <-> 
C R D ) )
51, 4mpbid 201 1  |-  ( ph  ->  C R D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  ofrval  6104  difsnen  6960  domunsncan  6978  phplem2  7057  infdifsn  7373  ltaddnq  8614  lemul2a  9627  xleadd2a  10590  xlemul2a  10625  monoord2  11093  expubnd  11178  bernneq2  11244  hashfun  11405  sqrlem2  11745  abs2dif2  11833  rlimdiv  12135  isercolllem1  12154  iseraltlem2  12171  iseraltlem3  12172  fsum00  12272  seqabs  12288  cvgcmp  12290  mertenslem1  12356  eftlub  12405  eirrlem  12498  prmreclem1  12979  efgcpbl2  15082  pgpfaclem2  15333  unitgrp  15465  xblss2  17974  xmstri2  18028  mstri2  18029  xmstri  18030  mstri  18031  xmstri3  18032  mstri3  18033  msrtri  18034  nrmmetd  18113  nmtri  18163  nmoi2  18255  xrsxmet  18331  xrge0gsumle  18354  iccpnfhmeo  18459  pcorev2  18542  pi1cpbl  18558  ovoliunlem1  18877  voliunlem3  18925  uniioombllem2  18954  dyadss  18965  dvlipcn  19357  dv11cn  19364  dvle  19370  dvfsumge  19385  dvfsumlem2  19390  dvfsumlem4  19392  dvfsum2  19397  dgrsub  19669  vieta1lem2  19707  itgulm2  19801  radcnvlem1  19805  abelthlem7  19830  efcvx  19841  logdivlti  19987  logcnlem4  20008  logccv  20026  cxple2a  20062  cxpaddlelem  20107  cxpaddle  20108  leibpi  20254  scvxcvx  20296  amgmlem  20300  ftalem2  20327  ppip1le  20415  ppieq0  20430  ppiltx  20431  chpeq0  20463  chtublem  20466  chtub  20467  logexprlim  20480  perfectlem2  20485  bposlem9  20547  2sqlem8  20627  chebbnd1lem1  20634  vmadivsum  20647  rplogsumlem1  20649  dchrisum0re  20678  dchrisum0lem1  20681  selberglem2  20711  chpdifbndlem1  20718  selberg3lem1  20722  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem6  20748  pntpbnd2  20752  pntibndlem2  20756  pntlemb  20762  pntlemr  20767  pntlemo  20772  ostth2lem2  20799  ostth2lem3  20800  occllem  21898  nmcexi  22622  cnlnadjlem7  22669  hmopidmchi  22747  subfaclim  23734  ovoliunnfl  25001  itg2addnc  25005  cntotbnd  26623  rrnmet  26656  jm2.24nn  27149  jm2.27a  27201  idomrootle  27614  stoweidlem10  27862  stoweidlem11  27863  stoweidlem14  27866  stoweidlem28  27880  3atlem1  30294  3atlem2  30295  llncvrlpln2  30368  lplncvrlvol2  30426  dalem25  30509  dalawlem7  30688  dalawlem11  30692  cdleme22g  31159  cdlemg18b  31490  cdlemg46  31546  dia2dimlem3  31878  dihord2  32039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator