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  2758  frecsuclem  6389  indpi  7308  cauappcvgprlemladdru  7622  prsrlt  7753  lesub2  8380  ltsub2  8382  rec11ap  8631  avglt1  9120  rpnegap  9647  modqmuladdnn0  10328  expap0  10510  2shfti  10799  mulreap  10832  minmax  11197  lemininf  11201  xrminmax  11232  xrlemininf  11238  modremain  11892  nn0seqcvgd  11999  divgcdcoprm0  12059  ismgmid  12635  grpsubeq0  12789  grpsubadd  12791  isxmet2d  13227  xblss2  13284  neibl  13370  ellimc3apf  13508  logbgt0b  13763  lgsne0  13818  lgsabs1  13819  iswomninnlem  14166