Theorem breq12i 5119

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

Syntax hints:   ↔ wb 206   = wceq 1540   class class class wbr 5110

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  3brtr3g  5143  3brtr4g  5144  caovord2  7604  domunfican  9279  ltsonq  10929  ltanq  10931  ltmnq  10932  prlem934  10993  prlem936  11007  ltsosr  11054  ltasr  11060  ltneg  11685  leneg  11688  lt2sqi  14161  le2sqi  14162  nn0le2msqi  14239  2sqreuop  27380  2sqreuopnn  27381  2sqreuoplt  27382  2sqreuopltb  27383  2sqreuopnnlt  27384  2sqreuopnnltb  27385  axlowdimlem6  28881  upgrwlkcompim  29578  clwlkcompbp  29719  mdsldmd1i  32267  fldext2chn  33725  constrextdg2lem  33745  divcnvlin  35727  ditgeq123i  36204  cbvditgvw2  36244  relowlpssretop  37359  2ap1caineq  42140  fsumlessf  45582  climlimsupcex  45774  liminfltlimsupex  45786  liminflelimsupcex  45802  sge0xaddlem2  46439  eubrdm  47041  isgrlim2  47986  iscmgmALT  48216  iscsgrpALT  48218