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  2753  frecsuclem  6374  indpi  7283  cauappcvgprlemladdru  7597  prsrlt  7728  lesub2  8355  ltsub2  8357  rec11ap  8606  avglt1  9095  rpnegap  9622  modqmuladdnn0  10303  expap0  10485  2shfti  10773  mulreap  10806  minmax  11171  lemininf  11175  xrminmax  11206  xrlemininf  11212  modremain  11866  nn0seqcvgd  11973  divgcdcoprm0  12033  ismgmid  12608  isxmet2d  12988  xblss2  13045  neibl  13131  ellimc3apf  13269  logbgt0b  13524  lgsne0  13579  lgsabs1  13580  iswomninnlem  13928