Theorem 3brtr4d 2645

Description: Substitution of equality into both sides of a binary relation.

Hypotheses

Ref	Expression
3brtr4d.1	|- (ph -> ARB)
3brtr4d.2	|- (ph -> C = A)
3brtr4d.3	|- (ph -> D = B)

Assertion

Ref	Expression
3brtr4d	|- (ph -> CRD)

Proof of Theorem 3brtr4d

Step	Hyp	Ref	Expression
1		3brtr4d.1	. 2 |- (ph -> ARB)
2		3brtr4d.2	. . 3 |- (ph -> C = A)
3		3brtr4d.3	. . 3 |- (ph -> D = B)
4	2, 3	breq12d 2631	. 2 |- (ph -> (CRD <-> ARB))
5	1, 4	mpbird 196	1 |- (ph -> CRD)

Syntax hints:   -> wi 3   = wceq 956   class class class wbr 2619

This theorem is referenced by:  lediv12it 5896  recp1lt1 5901  quoremz 6251  quoremOLD 6252  intfracqOLD 6255  expmwordit 6606  bernneq 6652  absrelet 6869  absimlet 6870  abs2difabst 6903  ser1absdiflem 6929  faclbnd 6945  faclbnd4lem3 6950  faclbnd4lem4 6951  faclbnd6 6954  fsumcmp 7040  fsumabs 7043  climsqueeze 7140  climsqueeze2 7141  ser1cmp 7174  ser1cmp2 7177  cvgcmp2lem 7180  isumcmpi 7215  erelem3 7321  efaddlem14 7351  ef1tllem 7381  ef01tllem2 7384  ef01tllem2OLD 7385  eflegeolem2 7414  ruclem24 7533  cnmet 7904  dscmet 7918  nvmtri 8299  imsmetlem 8323  nmlnoubi 8456  blometi 8463  ipblnfi 8516  ubthlem11 8539  hhssnv 9134  nmopco 10028  nmopcoadj 10034  idleop 10064  hmopidmch 10079  cdj1 10360  mslb1 10629

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620

Copyright terms: Public domain