Theorem breq12i 5094

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  3brtr3g  5118  3brtr4g  5119  caovord2  7579  domunfican  9232  ltsonq  10892  ltanq  10894  ltmnq  10895  prlem934  10956  prlem936  10970  ltsosr  11017  ltasr  11023  ltneg  11650  leneg  11653  lt2sqi  14151  le2sqi  14152  nn0le2msqi  14229  2sqreuop  27425  2sqreuopnn  27426  2sqreuoplt  27427  2sqreuopltb  27428  2sqreuopnnlt  27429  2sqreuopnnltb  27430  axlowdimlem6  29016  upgrwlkcompim  29711  clwlkcompbp  29850  mdsldmd1i  32402  fldext2chn  33872  constrextdg2lem  33892  divcnvlin  35915  ditgeq123i  36391  cbvditgvw2  36431  relowlpssretop  37680  2ap1caineq  42584  fsumlessf  46007  climlimsupcex  46197  liminfltlimsupex  46209  liminflelimsupcex  46225  sge0xaddlem2  46862  eubrdm  47484  isgrlim2  48459  iscmgmALT  48700  iscsgrpALT  48702