Theorem 3brtr4d 3925

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

Syntax hints:   -> wi 4   = wceq 1314   class class class wbr 3895

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-un 3041  df-sn 3499  df-pr 3500  df-op 3502  df-br 3896

This theorem is referenced by:  f1oiso2  5682  prarloclemarch2  7175  caucvgprprlemmu  7451  caucvgsrlembound  7536  mulap0  8328  lediv12a  8562  recp1lt1  8567  xleadd1a  9549  fldiv4p1lem1div2  9971  intfracq  9986  modqmulnn  10008  addmodlteq  10064  frecfzennn  10092  monoord2  10143  expgt1  10224  leexp2r  10240  leexp1a  10241  bernneq  10305  faclbnd  10380  faclbnd6  10383  facubnd  10384  hashunlem  10443  zfz1isolemiso  10475  sqrtgt0  10698  absrele  10747  absimle  10748  abstri  10768  abs2difabs  10772  bdtrilem  10902  bdtri  10903  xrmaxifle  10907  xrmaxadd  10922  xrbdtri  10937  climsqz  10996  climsqz2  10997  fsum3cvg2  11055  isumle  11156  expcnvap0  11163  expcnvre  11164  explecnv  11166  cvgratz  11193  efcllemp  11215  ege2le3  11228  eflegeo  11259  phibnd  11738  psmetres2  12322  xmetres2  12368  comet  12488  bdxmet  12490  cnmet  12519  limcimolemlt  12589  cvgcmp2nlemabs  12919  trilpolemlt1  12926