Theorem breq12i 4410

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	|- A = B
breq12i.2	|- C = D

Assertion

Ref	Expression
breq12i	|- ( A R C <-> B R D )

Proof of Theorem breq12i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 |- A = B
2		breq12i.2	. 2 |- C = D
3		breq12 4406	. 2 |- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
4	1, 2, 3	mp2an 672	1 |- ( A R C <-> B R D )

Syntax hints:   <-> wb 184   = wceq 1370   class class class wbr 4401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-br 4402

This theorem is referenced by:  3brtr3g  4432  3brtr4g  4433  caovord2  6386  domunfican  7696  ltsonq  9250  ltanq  9252  ltmnq  9253  prlem934  9314  prlem936  9328  ltsosr  9373  ltasr  9379  ltneg  9951  leneg  9954  inelr  10424  lt2sqi  12072  le2sqi  12073  nn0le2msqi  12163  axlowdimlem6  23346  mdsldmd1i  25888  divcnvlin  27544