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

Theorem 3brtr3d 4476
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 4460 . 2  |-  ( ph  ->  ( A R B  <-> 
C R D ) )
51, 4mpbid 210 1  |-  ( ph  ->  C R D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  ofrval  6534  difsnen  7599  domunsncan  7617  phplem2  7697  infdifsn  8073  ltaddnq  9352  lemul2a  10397  xleadd2a  11446  xlemul2a  11481  monoord2  12106  expubnd  12194  bernneq2  12261  hashfun  12461  sqrlem2  13040  abs2dif2  13129  rlimdiv  13431  isercolllem1  13450  iseraltlem2  13468  iseraltlem3  13469  fsum00  13575  seqabs  13591  cvgcmp  13593  mertenslem1  13656  eftlub  13705  eirrlem  13798  bitscmp  13947  prmreclem1  14293  efgcpbl2  16581  pgpfaclem2  16935  unitgrp  17117  xblss2  20668  xmstri2  20732  mstri2  20733  xmstri  20734  mstri  20735  xmstri3  20736  mstri3  20737  msrtri  20738  nrmmetd  20858  nmtri  20908  nmoi2  21000  xrsxmet  21077  xrge0gsumle  21101  iccpnfhmeo  21208  pcorev2  21291  pi1cpbl  21307  rrxmet  21598  ovoliunlem1  21676  voliunlem3  21725  uniioombllem2  21755  dyadss  21766  dvlipcn  22158  dv11cn  22165  dvle  22171  dvfsumge  22186  dvfsumlem2  22191  dvfsumlem4  22193  dvfsum2  22198  dgrsub  22431  vieta1lem2  22469  itgulm2  22566  radcnvlem1  22570  abelthlem7  22595  efcvx  22606  logdivlti  22761  logcnlem4  22782  logccv  22800  cxple2a  22836  cxpaddlelem  22881  cxpaddle  22882  leibpi  23029  scvxcvx  23071  amgmlem  23075  logdiflbnd  23080  ftalem2  23103  ppip1le  23191  ppieq0  23206  ppiltx  23207  chpeq0  23239  chtublem  23242  chtub  23243  logexprlim  23256  perfectlem2  23261  bposlem9  23323  2sqlem8  23403  chebbnd1lem1  23410  vmadivsum  23423  rplogsumlem1  23425  dchrisum0re  23454  dchrisum0lem1  23457  selberglem2  23487  chpdifbndlem1  23494  selberg3lem1  23498  pntrlog2bndlem2  23519  pntrlog2bndlem3  23520  pntrlog2bndlem6  23524  pntpbnd2  23528  pntibndlem2  23532  pntlemb  23538  pntlemr  23543  pntlemo  23548  ostth2lem2  23575  ostth2lem3  23576  legso  23740  krippenlem  23803  mideu  23842  occllem  25925  nmcexi  26649  cnlnadjlem7  26696  hmopidmchi  26774  omndadd2d  27388  omndmul2  27392  omndmul3  27393  ogrpinvOLD  27395  ogrpinv0le  27396  ogrpaddltrbid  27401  ogrpinv0lt  27403  isarchi3  27421  archirngz  27423  archiabllem1b  27426  gsumle  27461  orngsqr  27485  ornglmulle  27486  orngrmulle  27487  isarchiofld  27498  eulerpartlemgc  27969  dstfrvclim1  28084  lgamgulmlem2  28240  lgamgulmlem5  28243  lgambdd  28247  lgamcvg2  28265  subfaclim  28300  ovoliunnfl  29661  itg2addnclem3  29673  ftc1anclem8  29702  cntotbnd  29923  rrnmet  29956  jm2.24nn  30529  jm2.27a  30579  idomrootle  30785  stoweidlem10  31338  stoweidlem11  31339  stoweidlem13  31341  stoweidlem14  31342  stoweidlem28  31356  stirlinglem11  31412  stirlinglem12  31413  3atlem1  34297  3atlem2  34298  llncvrlpln2  34371  lplncvrlvol2  34429  dalem25  34512  dalawlem7  34691  dalawlem11  34695  cdleme22g  35162  cdlemg18b  35493  cdlemg46  35549  dia2dimlem3  35881  dihord2  36042
  Copyright terms: Public domain W3C validator