Theorem breq12i 2628

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 2624	. 2 |- ((A = B /\ C = D) -> (ARC <-> BRD))
4	1, 2, 3	mp2an 697	1 |- (ARC <-> BRD)

Syntax hints:   <-> wb 146   = wceq 956   class class class wbr 2619

This theorem is referenced by:  3brtr3g 2646  3brtr4g 2647  caoprord2 4057  ltsopq 5075  ltapq 5076  ltmpq 5077  ltaddpq 5079  prlem936a 5153  ltsosr 5203  ltasr 5209  ltpsrpr 5219  ltadd1 5591  leadd2 5593  ltneg 5603  lesub0 5612  ltdiv1i 5823  ltreci 5878  halfpos 5904  lt2sq 6624  le2sq 6625  discrlem1 6656  nn0le2msqt 6663  sqrlem16 6688  inelr 6735  reefiso 7428  ruclem2 7511  ruclem15 7524  pjthlem1 9219  mdsldmd1 10258

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620

Copyright terms: Public domain