Theorem breq12 3995

Description: Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)

Assertion

Ref	Expression
breq12	|- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )

Proof of Theorem breq12

Step	Hyp	Ref	Expression
1		breq1 3993	. 2 |- ( A = B -> ( A R C <-> B R C ) )
2		breq2 3994	. 2 |- ( C = D -> ( B R C <-> B R D ) )
3	1, 2	sylan9bb 460	1 |- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1349   class class class wbr 3990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-v 2733  df-un 3126  df-sn 3590  df-pr 3591  df-op 3593  df-br 3991

This theorem is referenced by:  breq12i  3999  breq12d  4003  breqan12d  4006  posng  4684  isopolem  5805  poxp  6215  rbropapd  6225  ecopover  6615  ecopoverg  6618  ltdcnq  7363  recexpr  7604  ltresr  7805  reapval  8499  ltxr  9736  xrltnr  9740  xrltnsym  9754  xrlttr  9756  xrltso  9757  xrlttri3  9758  xposdif  9843  exmidsbthrlem  14139