Theorem breq12i 5108

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

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

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  3brtr3g  5132  3brtr4g  5133  caovord2  7572  domunfican  9226  ltsonq  10884  ltanq  10886  ltmnq  10887  prlem934  10948  prlem936  10962  ltsosr  11009  ltasr  11015  ltneg  11641  leneg  11644  lt2sqi  14116  le2sqi  14117  nn0le2msqi  14194  2sqreuop  27433  2sqreuopnn  27434  2sqreuoplt  27435  2sqreuopltb  27436  2sqreuopnnlt  27437  2sqreuopnnltb  27438  axlowdimlem6  29024  upgrwlkcompim  29720  clwlkcompbp  29859  mdsldmd1i  32410  fldext2chn  33887  constrextdg2lem  33907  divcnvlin  35929  ditgeq123i  36405  cbvditgvw2  36445  relowlpssretop  37571  2ap1caineq  42467  fsumlessf  45890  climlimsupcex  46080  liminfltlimsupex  46092  liminflelimsupcex  46108  sge0xaddlem2  46745  eubrdm  47349  isgrlim2  48296  iscmgmALT  48537  iscsgrpALT  48539