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  2787  frecsuclem  6461  indpi  7404  cauappcvgprlemladdru  7718  prsrlt  7849  lesub2  8478  ltsub2  8480  rec11ap  8731  avglt1  9224  rpnegap  9755  modqmuladdnn0  10442  expap0  10643  2shfti  10978  mulreap  11011  minmax  11376  lemininf  11380  xrminmax  11411  xrlemininf  11417  modremain  12073  nnwosdc  12179  nn0seqcvgd  12182  divgcdcoprm0  12242  ismgmid  12963  grpsubeq0  13161  grpsubadd  13163  eqg0el  13302  isunitd  13605  lsslss  13880  isridlrng  13981  zndvds  14148  znleval  14152  isxmet2d  14527  xblss2  14584  neibl  14670  ellimc3apf  14839  logbgt0b  15139  lgsne0  15195  lgsabs1  15196  lgsquadlem1  15234  m1lgs  15242  iswomninnlem  15609