Theorem 3brtr4d 4036

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 4017	. 2 |- ( ph -> ( C R D <-> A R B ) )
5	1, 4	mpbird 167	1 |- ( ph -> C R D )

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 4004

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  f1oiso2  5828  prarloclemarch2  7418  caucvgprprlemmu  7694  caucvgsrlembound  7793  mulap0  8611  lediv12a  8851  recp1lt1  8856  xleadd1a  9873  fldiv4p1lem1div2  10305  intfracq  10320  modqmulnn  10342  addmodlteq  10398  frecfzennn  10426  monoord2  10477  expgt1  10558  leexp2r  10574  leexp1a  10575  bernneq  10641  faclbnd  10721  faclbnd6  10724  facubnd  10725  hashunlem  10784  zfz1isolemiso  10819  sqrtgt0  11043  absrele  11092  absimle  11093  abstri  11113  abs2difabs  11117  bdtrilem  11247  bdtri  11248  xrmaxifle  11254  xrmaxadd  11269  xrbdtri  11284  climsqz  11343  climsqz2  11344  fsum3cvg2  11402  isumle  11503  expcnvap0  11510  expcnvre  11511  explecnv  11513  cvgratz  11540  efcllemp  11666  ege2le3  11679  eflegeo  11709  cos12dec  11775  phibnd  12217  pcdvdstr  12326  pcprmpw2  12332  pockthg  12355  psmetres2  13836  xmetres2  13882  comet  14002  bdxmet  14004  cnmet  14033  ivthdec  14125  limcimolemlt  14136  tangtx  14262  logbgcd1irraplemap  14390  cvgcmp2nlemabs  14783  trilpolemlt1  14792