Theorem breq12i 5090

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

Syntax hints:   ↔ wb 205   = wceq 1539   class class class wbr 5081

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082

This theorem is referenced by:  3brtr3g  5114  3brtr4g  5115  caovord2  7516  domunfican  9131  ltsonq  10771  ltanq  10773  ltmnq  10774  prlem934  10835  prlem936  10849  ltsosr  10896  ltasr  10902  ltneg  11521  leneg  11524  inelr  12009  lt2sqi  13952  le2sqi  13953  nn0le2msqi  14027  2sqreuop  26655  2sqreuopnn  26656  2sqreuoplt  26657  2sqreuopltb  26658  2sqreuopnnlt  26659  2sqreuopnnltb  26660  axlowdimlem6  27360  upgrwlkcompim  28055  clwlkcompbp  28195  mdsldmd1i  30738  divcnvlin  33743  relowlpssretop  35579  2ap1caineq  40143  fsumlessf  43167  climlimsupcex  43359  liminfltlimsupex  43371  liminflelimsupcex  43387  sge0xaddlem2  44022  eubrdm  44588  iscmgmALT  45476  iscsgrpALT  45478