Theorem breq12i 5156

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

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

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 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  3brtr3g  5180  3brtr4g  5181  caovord2  7621  domunfican  9322  ltsonq  10966  ltanq  10968  ltmnq  10969  prlem934  11030  prlem936  11044  ltsosr  11091  ltasr  11097  ltneg  11718  leneg  11721  inelr  12206  lt2sqi  14157  le2sqi  14158  nn0le2msqi  14231  2sqreuop  27201  2sqreuopnn  27202  2sqreuoplt  27203  2sqreuopltb  27204  2sqreuopnnlt  27205  2sqreuopnnltb  27206  axlowdimlem6  28472  upgrwlkcompim  29167  clwlkcompbp  29306  mdsldmd1i  31851  divcnvlin  35006  relowlpssretop  36548  2ap1caineq  41267  fsumlessf  44591  climlimsupcex  44783  liminfltlimsupex  44795  liminflelimsupcex  44811  sge0xaddlem2  45448  eubrdm  46044  iscmgmALT  46900  iscsgrpALT  46902