Theorem 3brtr3d 4614

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

Step	Hyp	Ref	Expression
1		3brtr3d.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3		3brtr3d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	breq12d 4596	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷))
5	1, 4	mpbid 221	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

Syntax hints:   → wi 4   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  ofrval  6805  difsnen  7927  domunsncan  7945  phplem2  8025  infdifsn  8437  ltaddnq  9675  lemul2a  10757  mul2lt0rlt0  11808  xleadd2a  11956  xlemul2a  11991  monoord2  12694  expubnd  12783  bernneq2  12853  hashfun  13084  sqrlem2  13832  abs2dif2  13921  rlimdiv  14224  isercolllem1  14243  iseraltlem2  14261  iseraltlem3  14262  fsum00  14371  seqabs  14387  cvgcmp  14389  mertenslem1  14455  eftlub  14678  eirrlem  14771  bitscmp  14998  prmreclem1  15458  invisoinvl  16273  efgcpbl2  17993  pgpfaclem2  18304  unitgrp  18490  xblss2  22017  xmstri2  22081  mstri2  22082  xmstri  22083  mstri  22084  xmstri3  22085  mstri3  22086  msrtri  22087  nrmmetd  22189  nmtri  22240  nmoi2  22344  xrsxmet  22420  xrge0gsumle  22444  iccpnfhmeo  22552  pcorev2  22636  pi1cpbl  22652  rrxmet  22999  ovoliunlem1  23077  voliunlem3  23127  uniioombllem2  23157  dyadss  23168  dvlipcn  23561  dv11cn  23568  dvle  23574  dvfsumge  23589  dvfsumlem2  23594  dvfsumlem4  23596  dvfsum2  23601  dgrsub  23832  vieta1lem2  23870  itgulm2  23967  radcnvlem1  23971  abelthlem7  23996  efcvx  24007  logdivlti  24170  logcnlem4  24191  logccv  24209  cxple2a  24245  cxpaddlelem  24292  cxpaddle  24293  leibpi  24469  scvxcvx  24512  amgmlem  24516  logdiflbnd  24521  lgamgulmlem2  24556  lgamgulmlem5  24559  lgambdd  24563  lgamcvg2  24581  ftalem2  24600  ppip1le  24687  ppieq0  24702  ppiltx  24703  chpeq0  24733  chtublem  24736  chtub  24737  logexprlim  24750  perfectlem2  24755  bposlem9  24817  2sqlem8  24951  chebbnd1lem1  24958  vmadivsum  24971  rplogsumlem1  24973  dchrisum0re  25002  dchrisum0lem1  25005  selberglem2  25035  chpdifbndlem1  25042  selberg3lem1  25046  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem6  25072  pntpbnd2  25076  pntibndlem2  25080  pntlemb  25086  pntlemr  25091  pntlemo  25096  ostth2lem2  25123  ostth2lem3  25124  tgcgrsub2  25290  legso  25294  krippenlem  25385  midex  25429  opphllem3  25441  trgcopy  25496  occllem  27546  nmcexi  28269  cnlnadjlem7  28316  hmopidmchi  28394  omndadd2d  29039  omndmul2  29043  omndmul3  29044  ogrpinvOLD  29046  ogrpinv0le  29047  ogrpaddltbi  29050  ogrpaddltrbid  29052  ogrpinv0lt  29054  isarchi3  29072  archirngz  29074  archiabllem1b  29077  gsumle  29110  orngsqr  29135  ornglmulle  29136  orngrmulle  29137  isarchiofld  29148  esum2d  29482  omssubadd  29689  carsgclctun  29710  eulerpartlemgc  29751  dstfrvclim1  29866  subfaclim  30424  ovoliunnfl  32621  itg2addnclem3  32633  ftc1anclem8  32662  cntotbnd  32765  rrnmet  32798  3atlem1  33787  3atlem2  33788  llncvrlpln2  33861  lplncvrlvol2  33919  dalem25  34002  dalawlem7  34181  dalawlem11  34185  cdleme22g  34654  cdlemg18b  34985  cdlemg46  35041  dia2dimlem3  35373  dihord2  35534  jm2.24nn  36544  jm2.27a  36590  idomrootle  36792  amgm2d  37523  amgm3d  37524  amgm4d  37525  binomcxplemrat  37571  binomcxplemnotnn0  37577  ioossioobi  38590  ioodvbdlimc2lem  38824  stoweidlem10  38903  stoweidlem11  38904  stoweidlem13  38906  stoweidlem14  38907  stoweidlem28  38921  stirlinglem11  38977  stirlinglem12  38978  dirkercncflem4  38999  fourierdlem4  39004  fourierdlem6  39006  fourierdlem11  39011  fourierdlem42  39042  fourierdlem51  39050  fourierdlem73  39072  fourierdlem79  39078  2pwp1prm  40041  perfectALTVlem2  40165  fllogbd  42152  nnpw2blen  42172  amgmwlem  42357  amgmlemALT  42358  amgmw2d  42359  young2d  42360