Theorem 3brtr4d 4115

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)

Hypotheses

Ref	Expression
3brtr4d.1	|- ( ph -> A R B )
3brtr4d.2	|- ( ph -> C = A )
3brtr4d.3	|- ( ph -> D = B )

Assertion

Ref	Expression
3brtr4d	|- ( ph -> C R D )

Proof of Theorem 3brtr4d

Step	Hyp	Ref	Expression
1		3brtr4d.1	. 2 |- ( ph -> A R B )
2		3brtr4d.2	. . 3 |- ( ph -> C = A )
3		3brtr4d.3	. . 3 |- ( ph -> D = B )
4	2, 3	breq12d 4096	. 2 |- ( ph -> ( C R D <-> A R B ) )
5	1, 4	mpbird 167	1 |- ( ph -> C R D )

Syntax hints:   -> wi 4   = wceq 1395   class class class wbr 4083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  f1oiso2  5957  prarloclemarch2  7617  caucvgprprlemmu  7893  caucvgsrlembound  7992  mulap0  8812  lediv12a  9052  recp1lt1  9057  xleadd1a  10081  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  intfracq  10554  modqmulnn  10576  addmodlteq  10632  frecfzennn  10660  monoord2  10720  expgt1  10811  leexp2r  10827  leexp1a  10828  bernneq  10894  faclbnd  10975  faclbnd6  10978  facubnd  10979  hashunlem  11038  zfz1isolemiso  11074  sqrtgt0  11561  absrele  11610  absimle  11611  abstri  11631  abs2difabs  11635  bdtrilem  11766  bdtri  11767  xrmaxifle  11773  xrmaxadd  11788  xrbdtri  11803  climsqz  11862  climsqz2  11863  fsum3cvg2  11921  isumle  12022  expcnvap0  12029  expcnvre  12030  explecnv  12032  cvgratz  12059  efcllemp  12185  ege2le3  12198  eflegeo  12228  cos12dec  12295  fsumdvds  12369  phibnd  12755  pcdvdstr  12866  pcprmpw2  12872  pockthg  12896  2expltfac  12978  znrrg  14640  psmetres2  15023  xmetres2  15069  comet  15189  bdxmet  15191  cnmet  15220  ivthdec  15334  limcimolemlt  15354  tangtx  15528  logbgcd1irraplemap  15659  2lgslem1c  15785  cvgcmp2nlemabs  16488  trilpolemlt1  16497