Theorem 3brtr4d 4076

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 4057	. 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 4044

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045

This theorem is referenced by:  f1oiso2  5896  prarloclemarch2  7532  caucvgprprlemmu  7808  caucvgsrlembound  7907  mulap0  8727  lediv12a  8967  recp1lt1  8972  xleadd1a  9995  fldiv4p1lem1div2  10448  fldiv4lem1div2  10450  intfracq  10465  modqmulnn  10487  addmodlteq  10543  frecfzennn  10571  monoord2  10631  expgt1  10722  leexp2r  10738  leexp1a  10739  bernneq  10805  faclbnd  10886  faclbnd6  10889  facubnd  10890  hashunlem  10949  zfz1isolemiso  10984  sqrtgt0  11345  absrele  11394  absimle  11395  abstri  11415  abs2difabs  11419  bdtrilem  11550  bdtri  11551  xrmaxifle  11557  xrmaxadd  11572  xrbdtri  11587  climsqz  11646  climsqz2  11647  fsum3cvg2  11705  isumle  11806  expcnvap0  11813  expcnvre  11814  explecnv  11816  cvgratz  11843  efcllemp  11969  ege2le3  11982  eflegeo  12012  cos12dec  12079  fsumdvds  12153  phibnd  12539  pcdvdstr  12650  pcprmpw2  12656  pockthg  12680  2expltfac  12762  znrrg  14422  psmetres2  14805  xmetres2  14851  comet  14971  bdxmet  14973  cnmet  15002  ivthdec  15116  limcimolemlt  15136  tangtx  15310  logbgcd1irraplemap  15441  2lgslem1c  15567  cvgcmp2nlemabs  15971  trilpolemlt1  15980