Theorem breqan12d 2622

Description: Equality deduction for a binary relation.

Hypotheses

Ref	Expression
breq1d.1	|- (ph -> A = B)
breqan12i.2	|- (ps -> C = D)

Assertion

Ref	Expression
breqan12d	|- ((ph /\ ps) -> (ARC <-> BRD))

Proof of Theorem breqan12d

Step	Hyp	Ref	Expression
1		breq12 2614	. 2 |- ((A = B /\ C = D) -> (ARC <-> BRD))
2		breq1d.1	. 2 |- (ph -> A = B)
3		breqan12i.2	. 2 |- (ps -> C = D)
4	1, 2, 3	syl2an 454	1 |- ((ph /\ ps) -> (ARC <-> BRD))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   class class class wbr 2609

This theorem is referenced by:  breqan12rd 2623  isoid 3880  isotr 3882  isotrALT 3883  oprec 4302  pre-axltadd 5261  lemul1it 5793  lemul1itOLD 5794  expwordit 6534  lt2sqt 6561  le2sqt 6562  sqrle 6637  sqrlt 6638  ser1f0 7106  minveclem26 8501  minveclem27 8502  logltbt 8698  mddmdt 10138

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