Theorem 3brtr4d 2660

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 2646	. 2 |- (ph -> (CRD <-> ARB))
5	1, 4	mpbird 196	1 |- (ph -> CRD)

Syntax hints:   -> wi 3   = wceq 960   class class class wbr 2634

This theorem is referenced by:  lediv12a 5910  recp1lt1 5915  quoremz 6311  quoremnn0 6313  intfracq 6315  expmwordi 6637  bernneq 6683  absrele 6901  absimle 6902  abs2difabs 6935  ser1absdiflem 6961  faclbnd 6977  faclbnd4lem3 6982  faclbnd4lem4 6983  faclbnd6 6986  fsumcmp 7072  fsumabs 7075  climsqueezei 7172  climsqueeze2i 7173  ser1cmpi 7206  ser1cmp2i 7209  cvgcmp2lem 7212  isumcmpii 7247  erelem3 7353  efaddlem14 7383  ef1tllem 7413  ef01tllem2 7416  ef01tllem2OLD 7417  eflegeolem2 7446  ruclem24 7566  cnmet 7930  dscmet 7944  nvmtri 8324  imsmetlem 8348  nmlnoubi 8481  blometi 8488  ipblnfi 8541  ubthlem11 8564  hhssnv 9158  nmopcoi 10052  nmopcoadji 10058  idleop 10088  hmopidmchi 10103  cdj1i 10385  mslb1 10650

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-clab 1470  df-cleq 1475  df-clel 1478  df-v 1819  df-un 2061  df-sn 2424  df-pr 2425  df-op 2428  df-br 2635

Copyright terms: Public domain