Theorem breq12i 5115

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  3brtr3g  5141  3brtr4g  5142  caovord2  7654  domunfican  9338  ltsonq  11078  ltanq  11080  ltmnq  11081  prlem934  11142  prlem936  11156  ltsosr  11203  ltasr  11209  ltneg  11840  leneg  11843  lt2sqi  14356  le2sqi  14357  nn0le2msqi  14435  2sqreuop  27816  2sqreuopnn  27817  2sqreuoplt  27818  2sqreuopltb  27819  2sqreuopnnlt  27820  2sqreuopnnltb  27821  axlowdimlem6  29552  upgrwlkcompim  30250  clwlkcompbp  30396  mdsldmd1i  32960  fldext2chn  34427  constrextdg2lem  34447  divcnvlin  36675  ditgeq123i  37175  cbvditgvw2  37215  relowlpssretop  38478  2ap1caineq  43386  fsumlessf  46792  climlimsupcex  46982  liminfltlimsupex  46994  liminflelimsupcex  47010  sge0xaddlem2  47647  eubrdm  48309  isgrlim2  49284  iscmgmALT  49524  iscsgrpALT  49526