Theorem 3brtr4d 4034

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

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 4002

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4003

This theorem is referenced by:  f1oiso2  5825  prarloclemarch2  7415  caucvgprprlemmu  7691  caucvgsrlembound  7790  mulap0  8607  lediv12a  8847  recp1lt1  8852  xleadd1a  9869  fldiv4p1lem1div2  10300  intfracq  10315  modqmulnn  10337  addmodlteq  10393  frecfzennn  10421  monoord2  10472  expgt1  10553  leexp2r  10569  leexp1a  10570  bernneq  10635  faclbnd  10714  faclbnd6  10717  facubnd  10718  hashunlem  10777  zfz1isolemiso  10812  sqrtgt0  11036  absrele  11085  absimle  11086  abstri  11106  abs2difabs  11110  bdtrilem  11240  bdtri  11241  xrmaxifle  11247  xrmaxadd  11262  xrbdtri  11277  climsqz  11336  climsqz2  11337  fsum3cvg2  11395  isumle  11496  expcnvap0  11503  expcnvre  11504  explecnv  11506  cvgratz  11533  efcllemp  11659  ege2le3  11672  eflegeo  11702  cos12dec  11768  phibnd  12209  pcdvdstr  12318  pcprmpw2  12324  pockthg  12347  psmetres2  13704  xmetres2  13750  comet  13870  bdxmet  13872  cnmet  13901  ivthdec  13993  limcimolemlt  14004  tangtx  14130  logbgcd1irraplemap  14258  cvgcmp2nlemabs  14640  trilpolemlt1  14649