Theorem breq12d 2073

Description: Equality deduction for binary relation.

Hypotheses

Ref	Expression
breq1d.1	⊢ (φ → A = B)
breq12d.2	⊢ (φ → C = D)

Assertion

Ref	Expression
breq12d	⊢ (φ → (ARC ↔ BRD))

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. . 3 ⊢ (φ → A = B)
2	1	breq1d 2071	. 2 ⊢ (φ → (ARC ↔ BRC))
3		breq12d.2	. . 3 ⊢ (φ → C = D)
4	3	breq2d 2072	. 2 ⊢ (φ → (BRC ↔ BRD))
5	2, 4	bitrd 406	1 ⊢ (φ → (ARC ↔ BRD))

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091   class class class wbr 2054

This theorem is referenced by:  3brtr3d 2086  pocl 2132  isoeq1 2925  isocnv 2934  isotr 2935  isotrALT 2936  caoprord 3070  xpsneng 3340  limensuc 3402  pssnn 3428  unfi 3441  infensuc 3484  unxpdom 3650  sucxpdom 3652  ltapq 3870  ltmpq 3871  reclem4pr 3953  ltasr 4003  sqgt0sr 4009  axltadd 4085  axmulgt0 4086  ltadd1t 4348  ltadd2t 4349  leadd1t 4350  leadd2t 4351  lesub1t 4352  lesub0t 4374  ltmul1 4394  ltdiv 4399  ltdivt 4404  halfpost 4508  znnsubt 4595  uzind 4603  ruclem24 4908  ruclem25 4909  ruclem29 4913  norm3adift 5098  occllem2 5181  projlem22 5214  projlem26 5218  pjdifnormt 5637  pjnormt 5666  pjnelt 5667  cvexcht 5763

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063

metamath.org