Theorem breq12i 4465

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 4461	. 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 1395   class class class wbr 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457

This theorem is referenced by:  3brtr3g  4487  3brtr4g  4488  caovord2  6486  domunfican  7811  ltsonq  9364  ltanq  9366  ltmnq  9367  prlem934  9428  prlem936  9442  ltsosr  9488  ltasr  9494  ltneg  10073  leneg  10076  inelr  10546  lt2sqi  12259  le2sqi  12260  nn0le2msqi  12350  axlowdimlem6  24377  mdsldmd1i  27377  divcnvlin  29336  iscmgmALT  32810  iscsgrpALT  32812