Theorem breq12i 5120

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

Syntax hints:   ↔ wb 209   = wceq 1567   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112

This theorem is referenced by:  3brtr3g  5146  3brtr4g  5147  caovord2  7623  domunfican  9281  ltsonq  10954  ltanq  10956  ltmnq  10957  prlem934  11018  prlem936  11032  ltsosr  11079  ltasr  11085  ltneg  11714  leneg  11717  lt2sqi  14225  le2sqi  14226  nn0le2msqi  14303  2sqreuop  27592  2sqreuopnn  27593  2sqreuoplt  27594  2sqreuopltb  27595  2sqreuopnnlt  27596  2sqreuopnnltb  27597  axlowdimlem6  29238  upgrwlkcompim  29933  clwlkcompbp  30072  mdsldmd1i  32624  fldext2chn  34063  constrextdg2lem  34083  divcnvlin  36158  ditgeq123i  36644  cbvditgvw2  36684  relowlpssretop  37933  2ap1caineq  42837  fsumlessf  46220  climlimsupcex  46410  liminfltlimsupex  46422  liminflelimsupcex  46438  sge0xaddlem2  47075  eubrdm  47697  isgrlim2  48672  iscmgmALT  48913  iscsgrpALT  48915