Theorem syl2anbr 456

Description: A double syllogism inference.

Hypotheses

Ref	Expression
sylan.1	|- ((ph /\ ps) -> ch)
syl2anbr.2	|- (ph <-> th)
syl2anbr.3	|- (ps <-> ta)

Assertion

Ref	Expression
syl2anbr	|- ((th /\ ta) -> ch)

Proof of Theorem syl2anbr

Step	Hyp	Ref	Expression
1		sylan.1	. . 3 |- ((ph /\ ps) -> ch)
2		syl2anbr.2	. . 3 |- (ph <-> th)
3	1, 2	sylanbr 450	. 2 |- ((th /\ ps) -> ch)
4		syl2anbr.3	. 2 |- (ps <-> ta)
5	3, 4	sylan2br 453	1 |- ((th /\ ta) -> ch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  sylancbr 474  tz6.12 3722  rankelun 4679  brdom7disj 4776  brdom6disj 4777  cdaen 4896  ltresr 5230  alephadd 7524  opnin 7809  bcthlem32 7964  efifolem2 8638  sshjvalt 9235  sshjval3t 9241  hosmvalt 9428  hodmvalt 9430  hfsmvalt 9431

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain