Theorem 3brtr4d 4065

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

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4033

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034

This theorem is referenced by:  f1oiso2  5874  prarloclemarch2  7486  caucvgprprlemmu  7762  caucvgsrlembound  7861  mulap0  8681  lediv12a  8921  recp1lt1  8926  xleadd1a  9948  fldiv4p1lem1div2  10395  fldiv4lem1div2  10397  intfracq  10412  modqmulnn  10434  addmodlteq  10490  frecfzennn  10518  monoord2  10578  expgt1  10669  leexp2r  10685  leexp1a  10686  bernneq  10752  faclbnd  10833  faclbnd6  10836  facubnd  10837  hashunlem  10896  zfz1isolemiso  10931  sqrtgt0  11199  absrele  11248  absimle  11249  abstri  11269  abs2difabs  11273  bdtrilem  11404  bdtri  11405  xrmaxifle  11411  xrmaxadd  11426  xrbdtri  11441  climsqz  11500  climsqz2  11501  fsum3cvg2  11559  isumle  11660  expcnvap0  11667  expcnvre  11668  explecnv  11670  cvgratz  11697  efcllemp  11823  ege2le3  11836  eflegeo  11866  cos12dec  11933  fsumdvds  12007  phibnd  12385  pcdvdstr  12496  pcprmpw2  12502  pockthg  12526  2expltfac  12608  znrrg  14216  psmetres2  14569  xmetres2  14615  comet  14735  bdxmet  14737  cnmet  14766  ivthdec  14880  limcimolemlt  14900  tangtx  15074  logbgcd1irraplemap  15205  2lgslem1c  15331  cvgcmp2nlemabs  15676  trilpolemlt1  15685