Theorem breq12i 2633

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

Syntax hints:   <-> wb 146   = wceq 958   class class class wbr 2624

This theorem is referenced by:  3brtr3g 2651  3brtr4g 2652  caoprord2 4063  ltsopq 5087  ltapq 5088  ltmpq 5089  ltaddpq 5091  prlem936a 5165  ltsosr 5215  ltasr 5221  ltpsrpr 5231  ltadd1 5603  leadd2 5605  ltneg 5615  lesub0 5624  ltdiv1i 5825  ltreci 5880  halfpos 5906  lt2sq 6625  le2sq 6626  discrlem1 6657  nn0le2msqt 6664  sqrlem16 6689  inelr 6736  reefiso 7428  ruclem2 7512  ruclem15 7525  pjthlem1 9214  mdsldmd1 10253

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053  df-sn 2416  df-pr 2417  df-op 2420  df-br 2625

Copyright terms: Public domain