Theorem breq12i 5106

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 5102	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	mp2an 693	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)

Syntax hints:   ↔ wb 206   = wceq 1542   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  3brtr3g  5130  3brtr4g  5131  caovord2  7570  domunfican  9224  ltsonq  10882  ltanq  10884  ltmnq  10885  prlem934  10946  prlem936  10960  ltsosr  11007  ltasr  11013  ltneg  11639  leneg  11642  lt2sqi  14114  le2sqi  14115  nn0le2msqi  14192  2sqreuop  27431  2sqreuopnn  27432  2sqreuoplt  27433  2sqreuopltb  27434  2sqreuopnnlt  27435  2sqreuopnnltb  27436  axlowdimlem6  29001  upgrwlkcompim  29697  clwlkcompbp  29836  mdsldmd1i  32387  fldext2chn  33864  constrextdg2lem  33884  divcnvlin  35906  ditgeq123i  36382  cbvditgvw2  36422  relowlpssretop  37538  2ap1caineq  42434  fsumlessf  45860  climlimsupcex  46050  liminfltlimsupex  46062  liminflelimsupcex  46078  sge0xaddlem2  46715  eubrdm  47319  isgrlim2  48266  iscmgmALT  48507  iscsgrpALT  48509