Theorem breq123d 5121

Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)

Hypotheses

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
breq123d.2	⊢ (𝜑 → 𝑅 = 𝑆)
breq123d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
breq123d	⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷))

Proof of Theorem breq123d

Step	Hyp	Ref	Expression
1		breq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
3	1, 2	breq12d 5120	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4		breq123d.2	. . 3 ⊢ (𝜑 → 𝑅 = 𝑆)
5	4	breqd 5118	. 2 ⊢ (𝜑 → (𝐵𝑅𝐷 ↔ 𝐵𝑆𝐷))
6	3, 5	bitrd 279	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  sbcbr123  5161  fmptco  7101  xpsle  17542  invfuc  17939  yonedainv  18242  opphllem3  28676  lmif  28712  islmib  28714  iscgra  28736  isinag  28765  fmptcof2  32581  submomnd  33024  sgnsv  33117  inftmrel  33134  isinftm  33135  submarchi  33140  rlocval  33210  suborng  33293  rprmval  33487  weiunlem1  36450  uncov  37595  iscvlat  39316  paddfval  39791  lhpset  39989  tendofset  40752  diaffval  41024  fnwe2val  43038  aomclem8  43050  afv2eq12d  47216