Theorem breq123d 4818

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 4817	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4		breq123d.2	. . 3 ⊢ (𝜑 → 𝑅 = 𝑆)
5	4	breqd 4815	. 2 ⊢ (𝜑 → (𝐵𝑅𝐷 ↔ 𝐵𝑆𝐷))
6	3, 5	bitrd 268	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   class class class wbr 4804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805

This theorem is referenced by:  sbcbr123  4858  fmptco  6559  xpsle  16443  invfuc  16835  yonedainv  17122  opphllem3  25840  lmif  25876  islmib  25878  iscgra  25900  isinag  25928  fmptcof2  29766  submomnd  30019  sgnsv  30036  inftmrel  30043  isinftm  30044  submarchi  30049  suborng  30124  uncov  33703  iscvlat  35113  paddfval  35586  lhpset  35784  tendofset  36548  diaffval  36821  fnwe2val  38121  aomclem8  38133