Theorem 3brtr3d 2644

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

Hypotheses

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

Assertion

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

Proof of Theorem 3brtr3d

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

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

This theorem is referenced by:  phplem2 4509  ltaddpq 5079  lemul2it 5839  lemul2itOLD 5840  expordit 6600  expubndt 6608  bernneq2 6653  ser1absdif 6930  serzcmp 7054  climmullem3 7122  climmullem4 7123  caucvg 7163  iserzabslem 7178  cvgratlem3 7252  metge0 7819  ubthlem12 8540  osumlem3 9580  nmcopexlem5 9955  nmcfnexlem5 9984  cnlnadjlem7 10006

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