Theorem breq12i 5087

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079

This theorem is referenced by:  3brtr3g  5111  3brtr4g  5112  caovord2  7475  domunfican  9048  ltsonq  10709  ltanq  10711  ltmnq  10712  prlem934  10773  prlem936  10787  ltsosr  10834  ltasr  10840  ltneg  11458  leneg  11461  inelr  11946  lt2sqi  13887  le2sqi  13888  nn0le2msqi  13962  2sqreuop  26591  2sqreuopnn  26592  2sqreuoplt  26593  2sqreuopltb  26594  2sqreuopnnlt  26595  2sqreuopnnltb  26596  axlowdimlem6  27296  upgrwlkcompim  27990  clwlkcompbp  28129  mdsldmd1i  30672  divcnvlin  33677  relowlpssretop  35514  2ap1caineq  40081  fsumlessf  43072  climlimsupcex  43264  liminfltlimsupex  43276  liminflelimsupcex  43292  sge0xaddlem2  43926  eubrdm  44481  iscmgmALT  45370  iscsgrpALT  45372