Theorem breq12i 4882

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

Syntax hints:   ↔ wb 198   = wceq 1658   class class class wbr 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4874

This theorem is referenced by:  3brtr3g  4906  3brtr4g  4907  caovord2  7106  domunfican  8502  ltsonq  10106  ltanq  10108  ltmnq  10109  prlem934  10170  prlem936  10184  ltsosr  10231  ltasr  10237  ltneg  10852  leneg  10855  inelr  11340  lt2sqi  13246  le2sqi  13247  nn0le2msqi  13347  axlowdimlem6  26246  upgrwlkcompim  26940  clwlkcompbp  27084  mdsldmd1i  29745  divcnvlin  32160  relowlpssretop  33757  fsumlessf  40604  climlimsupcex  40796  liminfltlimsupex  40808  liminflelimsupcex  40824  sge0xaddlem2  41442  eubrdm  41967  iscmgmALT  42707  iscsgrpALT  42709