Theorem breq123d 5106

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

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

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  sbcbr123  5146  fmptco  7063  xpsle  17483  invfuc  17884  yonedainv  18187  submomnd  20011  suborng  20761  opphllem3  28694  lmif  28730  islmib  28732  iscgra  28754  isinag  28783  fmptcof2  32601  sgnsv  33103  inftmrel  33123  isinftm  33124  submarchi  33129  rlocval  33200  rprmval  33454  weiunlem1  36446  uncov  37591  iscvlat  39312  paddfval  39786  lhpset  39984  tendofset  40747  diaffval  41019  fnwe2val  43032  aomclem8  43044  afv2eq12d  47209