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  2843  frecsuclem  6650  mapsnend  7065  indpi  7673  cauappcvgprlemladdru  7987  prsrlt  8118  lesub2  8748  ltsub2  8750  rec11ap  9001  avglt1  9494  rpnegap  10037  modqmuladdnn0  10754  expap0  10955  swrdspsleq  11384  2shfti  11541  mulreap  11574  minmax  11940  lemininf  11944  xrminmax  11975  xrlemininf  11981  modremain  12640  nnwosdc  12760  nn0seqcvgd  12763  divgcdcoprm0  12823  ballotfilemsima  13203  ismgmid  13640  grpsubeq0  13841  grpsubadd  13843  eqg0el  13982  isunitd  14351  lsslss  14655  isridlrng  14756  zndvds  14923  znleval  14927  isxmet2d  15339  xblss2  15396  neibl  15482  ellimc3apf  15651  logbgt0b  15957  lgsne0  16037  lgsabs1  16038  lgsquadlem1  16076  m1lgs  16084  eupth2lem2dc  16580  eupth2lem3lem4fi  16594  iswomninnlem  16960