Theorem 3brtr3d 5178

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 5160	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷))
5	1, 4	mpbid 231	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  ofrval  7684  difsnen  9055  domunsncan  9074  phplem2OLD  9220  infdifsn  9654  ltaddnq  10971  lemul2a  12073  mul2lt0rlt0  13080  xleadd2a  13237  xlemul2a  13272  monoord2  14003  expubnd  14146  bernneq2  14197  hashfun  14401  01sqrexlem2  15194  abs2dif2  15284  rlimdiv  15596  isercolllem1  15615  iseraltlem2  15633  iseraltlem3  15634  fsum00  15748  seqabs  15764  cvgcmp  15766  mertenslem1  15834  fprodle  15944  eftlub  16056  eirrlem  16151  bitscmp  16383  prmreclem1  16853  invisoinvl  17741  efgcpbl2  19666  pgpfaclem2  19993  unitgrp  20274  xblss2  24128  xmstri2  24192  mstri2  24193  xmstri  24194  mstri  24195  xmstri3  24196  mstri3  24197  msrtri  24198  nrmmetd  24303  nmtri  24355  nmoi2  24467  xrsxmet  24545  xrge0gsumle  24569  iccpnfhmeo  24690  pcorev2  24775  pi1cpbl  24791  rrxmet  25156  ovoliunlem1  25251  voliunlem3  25301  uniioombllem2  25332  dyadss  25343  dvlipcn  25746  dv11cn  25753  dvle  25759  dvfsumge  25774  dvfsumlem2  25779  dvfsumlem4  25781  dvfsum2  25786  dgrsub  26022  vieta1lem2  26060  itgulm2  26157  radcnvlem1  26161  abelthlem7  26186  efcvx  26197  logdivlti  26364  logcnlem4  26389  logccv  26407  cxple2a  26443  cxpaddlelem  26495  cxpaddle  26496  leibpi  26683  scvxcvx  26726  amgmlem  26730  logdiflbnd  26735  lgamgulmlem2  26770  lgamgulmlem5  26773  lgambdd  26777  lgamcvg2  26795  ftalem2  26814  ppip1le  26901  ppieq0  26916  ppiltx  26917  chpeq0  26947  chtublem  26950  chtub  26951  logexprlim  26964  perfectlem2  26969  bposlem9  27031  2sqlem8  27165  chebbnd1lem1  27208  vmadivsum  27221  rplogsumlem1  27223  dchrisum0re  27252  dchrisum0lem1  27255  selberglem2  27285  chpdifbndlem1  27292  selberg3lem1  27296  pntrlog2bndlem2  27317  pntrlog2bndlem3  27318  pntrlog2bndlem6  27322  pntpbnd2  27326  pntibndlem2  27330  pntlemb  27336  pntlemr  27341  pntlemo  27346  ostth2lem2  27373  ostth2lem3  27374  nosupbnd2lem1  27454  noinfbnd2lem1  27469  mulsgt0  27839  tgcgrsub2  28113  legso  28117  krippenlem  28208  midex  28255  opphllem3  28267  trgcopy  28322  occllem  30823  nmcexi  31546  cnlnadjlem7  31593  hmopidmchi  31671  mgcf1o  32440  omndadd2d  32496  omndmul2  32500  omndmul3  32501  ogrpinv0le  32503  ogrpaddltbi  32506  ogrpaddltrbid  32508  ogrpinv0lt  32510  gsumle  32512  isarchi3  32603  archirngz  32605  archiabllem1b  32608  orngsqr  32692  ornglmulle  32693  orngrmulle  32694  isarchiofld  32705  esum2d  33389  omssubadd  33597  carsgclctun  33618  eulerpartlemgc  33659  dstfrvclim1  33774  fdvneggt  33910  fdvnegge  33912  logdivsqrle  33960  hgt750lemb  33966  subfaclim  34477  gg-dvfsumlem2  35469  ovoliunnfl  36833  itg2addnclem3  36844  ftc1anclem8  36871  cntotbnd  36967  rrnmet  37000  3atlem1  38657  3atlem2  38658  llncvrlpln2  38731  lplncvrlvol2  38789  dalem25  38872  dalawlem7  39051  dalawlem11  39055  cdleme22g  39522  cdlemg18b  39853  cdlemg46  39909  dia2dimlem3  40240  dihord2  40401  3lexlogpow5ineq2  41226  3lexlogpow2ineq1  41229  3lexlogpow5ineq5  41231  aks4d1p1p7  41245  aks4d1p1  41247  aks4d1p6  41252  sticksstones6  41273  jm2.24nn  42000  jm2.27a  42046  idomrootle  42239  amgm2d  43252  amgm3d  43253  amgm4d  43254  binomcxplemrat  43411  binomcxplemnotnn0  43417  monoord2xrv  44492  ioossioobi  44528  ioodvbdlimc2lem  44948  stoweidlem10  45024  stoweidlem11  45025  stoweidlem13  45027  stoweidlem14  45028  stoweidlem28  45042  stirlinglem11  45098  stirlinglem12  45099  dirkercncflem4  45120  fourierdlem4  45125  fourierdlem6  45127  fourierdlem11  45132  fourierdlem42  45163  fourierdlem51  45171  fourierdlem73  45193  fourierdlem79  45199  2pwp1prm  46555  perfectALTVlem2  46688  fllogbd  47333  nnpw2blen  47353  amgmwlem  47936  amgmlemALT  47937  amgmw2d  47938  young2d  47939