Theorem breq12i 5101

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

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

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  3brtr3g  5125  3brtr4g  5126  caovord2  7561  domunfican  9211  ltsonq  10863  ltanq  10865  ltmnq  10866  prlem934  10927  prlem936  10941  ltsosr  10988  ltasr  10994  ltneg  11620  leneg  11623  lt2sqi  14096  le2sqi  14097  nn0le2msqi  14174  2sqreuop  27371  2sqreuopnn  27372  2sqreuoplt  27373  2sqreuopltb  27374  2sqreuopnnlt  27375  2sqreuopnnltb  27376  axlowdimlem6  28896  upgrwlkcompim  29592  clwlkcompbp  29731  mdsldmd1i  32279  fldext2chn  33711  constrextdg2lem  33731  divcnvlin  35726  ditgeq123i  36203  cbvditgvw2  36243  relowlpssretop  37358  2ap1caineq  42138  fsumlessf  45578  climlimsupcex  45770  liminfltlimsupex  45782  liminflelimsupcex  45798  sge0xaddlem2  46435  eubrdm  47040  isgrlim2  47987  iscmgmALT  48228  iscsgrpALT  48230