Theorem breq12i 2618

Description: Equality inference for a binary relation. (The proof was shortened by Eric Schmidt, 4-Apr-2007.)

Hypotheses

Ref	Expression
breq1i.1	|- A = B
breq12i.2	|- C = D

Assertion

Ref	Expression
breq12i	|- (ARC <-> BRD)

Proof of Theorem breq12i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 |- A = B
2		breq12i.2	. 2 |- C = D
3		breq12 2614	. 2 |- ((A = B /\ C = D) -> (ARC <-> BRD))
4	1, 2, 3	mp2an 695	1 |- (ARC <-> BRD)

Syntax hints:   <-> wb 146   = wceq 953   class class class wbr 2609

This theorem is referenced by:  3brtr3g 2636  3brtr4g 2637  caoprord2 4043  ltsopq 5047  ltapq 5048  ltmpq 5049  ltaddpq 5051  prlem936a 5125  ltsosr 5175  ltasr 5181  ltpsrpr 5191  ltadd1 5565  leadd2 5567  ltneg 5577  lesub0 5586  ltdiv1i 5779  ltreci 5826  halfpos 5852  lt2sq 6555  le2sq 6556  discrlem1 6586  nn0le2msqt 6593  sqrlem16 6618  inelr 6665  reefiso 7370  ruclem2 7454  ruclem15 7467  pjthlem1 9134  mdsldmd1 10166

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain