Theorem 3brtr4d 4120

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

Syntax hints:   -> wi 4   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  f1oiso2  5968  prarloclemarch2  7639  caucvgprprlemmu  7915  caucvgsrlembound  8014  mulap0  8834  lediv12a  9074  recp1lt1  9079  xleadd1a  10108  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  intfracq  10583  modqmulnn  10605  addmodlteq  10661  frecfzennn  10689  monoord2  10749  expgt1  10840  leexp2r  10856  leexp1a  10857  bernneq  10923  faclbnd  11004  faclbnd6  11007  facubnd  11008  hashunlem  11068  zfz1isolemiso  11104  sqrtgt0  11612  absrele  11661  absimle  11662  abstri  11682  abs2difabs  11686  bdtrilem  11817  bdtri  11818  xrmaxifle  11824  xrmaxadd  11839  xrbdtri  11854  climsqz  11913  climsqz2  11914  fsum3cvg2  11973  isumle  12074  expcnvap0  12081  expcnvre  12082  explecnv  12084  cvgratz  12111  efcllemp  12237  ege2le3  12250  eflegeo  12280  cos12dec  12347  fsumdvds  12421  phibnd  12807  pcdvdstr  12918  pcprmpw2  12924  pockthg  12948  2expltfac  13030  znrrg  14693  psmetres2  15076  xmetres2  15122  comet  15242  bdxmet  15244  cnmet  15273  ivthdec  15387  limcimolemlt  15407  tangtx  15581  logbgcd1irraplemap  15712  2lgslem1c  15838  cvgcmp2nlemabs  16687  trilpolemlt1  16696