Theorem breq12i 5116

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  3brtr3g  5140  3brtr4g  5141  caovord2  7601  domunfican  9272  ltsonq  10922  ltanq  10924  ltmnq  10925  prlem934  10986  prlem936  11000  ltsosr  11047  ltasr  11053  ltneg  11678  leneg  11681  lt2sqi  14154  le2sqi  14155  nn0le2msqi  14232  2sqreuop  27373  2sqreuopnn  27374  2sqreuoplt  27375  2sqreuopltb  27376  2sqreuopnnlt  27377  2sqreuopnnltb  27378  axlowdimlem6  28874  upgrwlkcompim  29571  clwlkcompbp  29712  mdsldmd1i  32260  fldext2chn  33718  constrextdg2lem  33738  divcnvlin  35720  ditgeq123i  36197  cbvditgvw2  36237  relowlpssretop  37352  2ap1caineq  42133  fsumlessf  45575  climlimsupcex  45767  liminfltlimsupex  45779  liminflelimsupcex  45795  sge0xaddlem2  46432  eubrdm  47037  isgrlim2  47982  iscmgmALT  48212  iscsgrpALT  48214