Theorem breq12i 5109

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  3brtr3g  5133  3brtr4g  5134  caovord2  7582  domunfican  9236  ltsonq  10894  ltanq  10896  ltmnq  10897  prlem934  10958  prlem936  10972  ltsosr  11019  ltasr  11025  ltneg  11651  leneg  11654  lt2sqi  14126  le2sqi  14127  nn0le2msqi  14204  2sqreuop  27446  2sqreuopnn  27447  2sqreuoplt  27448  2sqreuopltb  27449  2sqreuopnnlt  27450  2sqreuopnnltb  27451  axlowdimlem6  29038  upgrwlkcompim  29734  clwlkcompbp  29873  mdsldmd1i  32425  fldext2chn  33912  constrextdg2lem  33932  divcnvlin  35955  ditgeq123i  36431  cbvditgvw2  36471  relowlpssretop  37646  2ap1caineq  42544  fsumlessf  45966  climlimsupcex  46156  liminfltlimsupex  46168  liminflelimsupcex  46184  sge0xaddlem2  46821  eubrdm  47425  isgrlim2  48372  iscmgmALT  48613  iscsgrpALT  48615