Theorem 3bitr2d 216

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 191	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitr2d.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 188	1 |- ( ph -> ( ps <-> ta ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ceqsralt  2790  frecsuclem  6466  indpi  7412  cauappcvgprlemladdru  7726  prsrlt  7857  lesub2  8487  ltsub2  8489  rec11ap  8740  avglt1  9233  rpnegap  9764  modqmuladdnn0  10463  expap0  10664  2shfti  10999  mulreap  11032  minmax  11398  lemininf  11402  xrminmax  11433  xrlemininf  11439  modremain  12097  nnwosdc  12217  nn0seqcvgd  12220  divgcdcoprm0  12280  ismgmid  13046  grpsubeq0  13244  grpsubadd  13246  eqg0el  13385  isunitd  13688  lsslss  13963  isridlrng  14064  zndvds  14231  znleval  14235  isxmet2d  14610  xblss2  14667  neibl  14753  ellimc3apf  14922  logbgt0b  15228  lgsne0  15305  lgsabs1  15306  lgsquadlem1  15344  m1lgs  15352  iswomninnlem  15720