Theorem breq12i 5095

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

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

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  3brtr3g  5119  3brtr4g  5120  caovord2  7574  domunfican  9227  ltsonq  10887  ltanq  10889  ltmnq  10890  prlem934  10951  prlem936  10965  ltsosr  11012  ltasr  11018  ltneg  11645  leneg  11648  lt2sqi  14146  le2sqi  14147  nn0le2msqi  14224  2sqreuop  27443  2sqreuopnn  27444  2sqreuoplt  27445  2sqreuopltb  27446  2sqreuopnnlt  27447  2sqreuopnnltb  27448  axlowdimlem6  29034  upgrwlkcompim  29730  clwlkcompbp  29869  mdsldmd1i  32421  fldext2chn  33892  constrextdg2lem  33912  divcnvlin  35935  ditgeq123i  36411  cbvditgvw2  36451  relowlpssretop  37700  2ap1caineq  42604  fsumlessf  46031  climlimsupcex  46221  liminfltlimsupex  46233  liminflelimsupcex  46249  sge0xaddlem2  46886  eubrdm  47502  isgrlim2  48477  iscmgmALT  48718  iscsgrpALT  48720