Theorem breq12i 5157

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)

Hypotheses

Ref	Expression
breq1i.1	⊢ 𝐴 = 𝐵
breq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
breq12i	⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)

Proof of Theorem breq12i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		breq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		breq12 5153	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	mp2an 689	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)

Syntax hints:   ↔ wb 205   = wceq 1540   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  3brtr3g  5181  3brtr4g  5182  caovord2  7623  domunfican  9326  ltsonq  10970  ltanq  10972  ltmnq  10973  prlem934  11034  prlem936  11048  ltsosr  11095  ltasr  11101  ltneg  11721  leneg  11724  inelr  12209  lt2sqi  14160  le2sqi  14161  nn0le2msqi  14234  2sqreuop  27307  2sqreuopnn  27308  2sqreuoplt  27309  2sqreuopltb  27310  2sqreuopnnlt  27311  2sqreuopnnltb  27312  axlowdimlem6  28637  upgrwlkcompim  29332  clwlkcompbp  29471  mdsldmd1i  32016  divcnvlin  35171  relowlpssretop  36708  2ap1caineq  41427  fsumlessf  44751  climlimsupcex  44943  liminfltlimsupex  44955  liminflelimsupcex  44971  sge0xaddlem2  45608  eubrdm  46204  iscmgmALT  47060  iscsgrpALT  47062