Theorem 3bitr2d 215

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2d.1	|- ( ph -> ( ps <-> ch ) )
3bitr2d.2	|- ( ph -> ( th <-> ch ) )
3bitr2d.3	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
3bitr2d	|- ( ph -> ( ps <-> ta ) )

Proof of Theorem 3bitr2d

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		3bitr2d.2	. . 3 |- ( ph -> ( th <-> ch ) )
3	1, 2	bitr4d 190	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitr2d.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 187	1 |- ( ph -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ceqsralt  2739  frecsuclem  6350  indpi  7256  cauappcvgprlemladdru  7570  prsrlt  7701  lesub2  8326  ltsub2  8328  rec11ap  8577  avglt1  9065  rpnegap  9586  modqmuladdnn0  10260  expap0  10442  2shfti  10724  mulreap  10757  minmax  11122  lemininf  11126  xrminmax  11155  xrlemininf  11161  modremain  11812  nn0seqcvgd  11909  divgcdcoprm0  11969  isxmet2d  12719  xblss2  12776  neibl  12862  ellimc3apf  13000  logbgt0b  13254  iswomninnlem  13591