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

Theorem 3brtr3d 4791
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 4773 . 2 (𝜑 → (𝐴𝑅𝐵𝐶𝑅𝐷))
51, 4mpbid 222 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1596   class class class wbr 4760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-br 4761
This theorem is referenced by:  ofrval  7024  difsnen  8158  domunsncan  8176  phplem2  8256  infdifsn  8667  ltaddnq  9909  lemul2a  10991  mul2lt0rlt0  12046  xleadd2a  12198  xlemul2a  12233  monoord2  12947  expubnd  13036  bernneq2  13106  hashfun  13337  sqrlem2  14104  abs2dif2  14193  rlimdiv  14496  isercolllem1  14515  iseraltlem2  14533  iseraltlem3  14534  fsum00  14650  seqabs  14666  cvgcmp  14668  mertenslem1  14736  eftlub  14959  eirrlem  15052  bitscmp  15283  prmreclem1  15743  invisoinvl  16572  efgcpbl2  18291  pgpfaclem2  18602  unitgrp  18788  xblss2  22329  xmstri2  22393  mstri2  22394  xmstri  22395  mstri  22396  xmstri3  22397  mstri3  22398  msrtri  22399  nrmmetd  22501  nmtri  22552  nmoi2  22656  xrsxmet  22734  xrge0gsumle  22758  iccpnfhmeo  22866  pcorev2  22949  pi1cpbl  22965  rrxmet  23312  ovoliunlem1  23391  voliunlem3  23441  uniioombllem2  23472  dyadss  23483  dvlipcn  23877  dv11cn  23884  dvle  23890  dvfsumge  23905  dvfsumlem2  23910  dvfsumlem4  23912  dvfsum2  23917  dgrsub  24148  vieta1lem2  24186  itgulm2  24283  radcnvlem1  24287  abelthlem7  24312  efcvx  24323  logdivlti  24486  logcnlem4  24511  logccv  24529  cxple2a  24565  cxpaddlelem  24612  cxpaddle  24613  leibpi  24789  scvxcvx  24832  amgmlem  24836  logdiflbnd  24841  lgamgulmlem2  24876  lgamgulmlem5  24879  lgambdd  24883  lgamcvg2  24901  ftalem2  24920  ppip1le  25007  ppieq0  25022  ppiltx  25023  chpeq0  25053  chtublem  25056  chtub  25057  logexprlim  25070  perfectlem2  25075  bposlem9  25137  2sqlem8  25271  chebbnd1lem1  25278  vmadivsum  25291  rplogsumlem1  25293  dchrisum0re  25322  dchrisum0lem1  25325  selberglem2  25355  chpdifbndlem1  25362  selberg3lem1  25366  pntrlog2bndlem2  25387  pntrlog2bndlem3  25388  pntrlog2bndlem6  25392  pntpbnd2  25396  pntibndlem2  25400  pntlemb  25406  pntlemr  25411  pntlemo  25416  ostth2lem2  25443  ostth2lem3  25444  tgcgrsub2  25610  legso  25614  krippenlem  25705  midex  25749  opphllem3  25761  trgcopy  25816  occllem  28392  nmcexi  29115  cnlnadjlem7  29162  hmopidmchi  29240  omndadd2d  29938  omndmul2  29942  omndmul3  29943  ogrpinvOLD  29945  ogrpinv0le  29946  ogrpaddltbi  29949  ogrpaddltrbid  29951  ogrpinv0lt  29953  isarchi3  29971  archirngz  29973  archiabllem1b  29976  gsumle  30009  orngsqr  30034  ornglmulle  30035  orngrmulle  30036  isarchiofld  30047  esum2d  30385  omssubadd  30592  carsgclctun  30613  eulerpartlemgc  30654  dstfrvclim1  30769  fdvneggt  30908  fdvnegge  30910  logdivsqrle  30958  hgt750lemb  30964  subfaclim  31398  nosupbnd2lem1  32088  ovoliunnfl  33683  itg2addnclem3  33695  ftc1anclem8  33724  cntotbnd  33827  rrnmet  33860  3atlem1  35189  3atlem2  35190  llncvrlpln2  35263  lplncvrlvol2  35321  dalem25  35404  dalawlem7  35583  dalawlem11  35587  cdleme22g  36055  cdlemg18b  36386  cdlemg46  36442  dia2dimlem3  36774  dihord2  36935  jm2.24nn  37945  jm2.27a  37991  idomrootle  38192  amgm2d  38920  amgm3d  38921  amgm4d  38922  binomcxplemrat  38968  binomcxplemnotnn0  38974  monoord2xrv  40129  ioossioobi  40163  ioodvbdlimc2lem  40569  stoweidlem10  40647  stoweidlem11  40648  stoweidlem13  40650  stoweidlem14  40651  stoweidlem28  40665  stirlinglem11  40721  stirlinglem12  40722  dirkercncflem4  40743  fourierdlem4  40748  fourierdlem6  40750  fourierdlem11  40755  fourierdlem42  40786  fourierdlem51  40794  fourierdlem73  40816  fourierdlem79  40822  2pwp1prm  41930  perfectALTVlem2  42058  fllogbd  42781  nnpw2blen  42801  amgmwlem  42978  amgmlemALT  42979  amgmw2d  42980  young2d  42981
  Copyright terms: Public domain W3C validator