Theorem breq12i 5119

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

Syntax hints:   ↔ wb 205   = wceq 1541   class class class wbr 5110

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111

This theorem is referenced by:  3brtr3g  5143  3brtr4g  5144  caovord2  7571  domunfican  9271  ltsonq  10914  ltanq  10916  ltmnq  10917  prlem934  10978  prlem936  10992  ltsosr  11039  ltasr  11045  ltneg  11664  leneg  11667  inelr  12152  lt2sqi  14103  le2sqi  14104  nn0le2msqi  14177  2sqreuop  26847  2sqreuopnn  26848  2sqreuoplt  26849  2sqreuopltb  26850  2sqreuopnnlt  26851  2sqreuopnnltb  26852  axlowdimlem6  27959  upgrwlkcompim  28654  clwlkcompbp  28793  mdsldmd1i  31336  divcnvlin  34391  relowlpssretop  35908  2ap1caineq  40626  fsumlessf  43938  climlimsupcex  44130  liminfltlimsupex  44142  liminflelimsupcex  44158  sge0xaddlem2  44795  eubrdm  45390  iscmgmALT  46278  iscsgrpALT  46280