Theorem breq12i 5039

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

Syntax hints:   ↔ wb 209   = wceq 1538   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  3brtr3g  5063  3brtr4g  5064  caovord2  7340  domunfican  8775  ltsonq  10380  ltanq  10382  ltmnq  10383  prlem934  10444  prlem936  10458  ltsosr  10505  ltasr  10511  ltneg  11129  leneg  11132  inelr  11615  lt2sqi  13548  le2sqi  13549  nn0le2msqi  13623  2sqreuop  26046  2sqreuopnn  26047  2sqreuoplt  26048  2sqreuopltb  26049  2sqreuopnnlt  26050  2sqreuopnnltb  26051  axlowdimlem6  26741  upgrwlkcompim  27432  clwlkcompbp  27571  mdsldmd1i  30114  divcnvlin  33077  relowlpssretop  34781  3lexlogpow5ineq1  39341  2ap1caineq  39349  fsumlessf  42219  climlimsupcex  42411  liminfltlimsupex  42423  liminflelimsupcex  42439  sge0xaddlem2  43073  eubrdm  43628  iscmgmALT  44484  iscsgrpALT  44486