Theorem 3brtr4d 4091

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

Syntax hints:   -> wi 4   = wceq 1373   class class class wbr 4059

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  f1oiso2  5919  prarloclemarch2  7567  caucvgprprlemmu  7843  caucvgsrlembound  7942  mulap0  8762  lediv12a  9002  recp1lt1  9007  xleadd1a  10030  fldiv4p1lem1div2  10485  fldiv4lem1div2  10487  intfracq  10502  modqmulnn  10524  addmodlteq  10580  frecfzennn  10608  monoord2  10668  expgt1  10759  leexp2r  10775  leexp1a  10776  bernneq  10842  faclbnd  10923  faclbnd6  10926  facubnd  10927  hashunlem  10986  zfz1isolemiso  11021  sqrtgt0  11460  absrele  11509  absimle  11510  abstri  11530  abs2difabs  11534  bdtrilem  11665  bdtri  11666  xrmaxifle  11672  xrmaxadd  11687  xrbdtri  11702  climsqz  11761  climsqz2  11762  fsum3cvg2  11820  isumle  11921  expcnvap0  11928  expcnvre  11929  explecnv  11931  cvgratz  11958  efcllemp  12084  ege2le3  12097  eflegeo  12127  cos12dec  12194  fsumdvds  12268  phibnd  12654  pcdvdstr  12765  pcprmpw2  12771  pockthg  12795  2expltfac  12877  znrrg  14537  psmetres2  14920  xmetres2  14966  comet  15086  bdxmet  15088  cnmet  15117  ivthdec  15231  limcimolemlt  15251  tangtx  15425  logbgcd1irraplemap  15556  2lgslem1c  15682  cvgcmp2nlemabs  16173  trilpolemlt1  16182