Theorem breq12i 5133

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5124

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  3brtr3g  5157  3brtr4g  5158  caovord2  7624  domunfican  9338  ltsonq  10988  ltanq  10990  ltmnq  10991  prlem934  11052  prlem936  11066  ltsosr  11113  ltasr  11119  ltneg  11742  leneg  11745  inelr  12235  lt2sqi  14212  le2sqi  14213  nn0le2msqi  14290  2sqreuop  27430  2sqreuopnn  27431  2sqreuoplt  27432  2sqreuopltb  27433  2sqreuopnnlt  27434  2sqreuopnnltb  27435  axlowdimlem6  28931  upgrwlkcompim  29628  clwlkcompbp  29769  mdsldmd1i  32317  fldext2chn  33767  constrextdg2lem  33787  divcnvlin  35755  ditgeq123i  36232  cbvditgvw2  36272  relowlpssretop  37387  2ap1caineq  42163  fsumlessf  45573  climlimsupcex  45765  liminfltlimsupex  45777  liminflelimsupcex  45793  sge0xaddlem2  46430  eubrdm  47032  isgrlim2  47962  iscmgmALT  48166  iscsgrpALT  48168