Theorem breq12i 5111

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

Syntax hints:   ↔ wb 208   = wceq 1562   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  3brtr3g  5135  3brtr4g  5136  caovord2  7610  domunfican  9268  ltsonq  10929  ltanq  10931  ltmnq  10932  prlem934  10993  prlem936  11007  ltsosr  11054  ltasr  11060  ltneg  11689  leneg  11692  lt2sqi  14204  le2sqi  14205  nn0le2msqi  14282  2sqreuop  27528  2sqreuopnn  27529  2sqreuoplt  27530  2sqreuopltb  27531  2sqreuopnnlt  27532  2sqreuopnnltb  27533  axlowdimlem6  29150  upgrwlkcompim  29845  clwlkcompbp  29984  mdsldmd1i  32536  fldext2chn  34027  constrextdg2lem  34047  divcnvlin  36088  ditgeq123i  36574  cbvditgvw2  36614  relowlpssretop  37863  2ap1caineq  42767  fsumlessf  46158  climlimsupcex  46348  liminfltlimsupex  46360  liminflelimsupcex  46376  sge0xaddlem2  47013  eubrdm  47635  isgrlim2  48610  iscmgmALT  48851  iscsgrpALT  48853