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  2827  frecsuclem  6558  indpi  7540  cauappcvgprlemladdru  7854  prsrlt  7985  lesub2  8615  ltsub2  8617  rec11ap  8868  avglt1  9361  rpnegap  9894  modqmuladdnn0  10602  expap0  10803  swrdspsleq  11214  2shfti  11357  mulreap  11390  minmax  11756  lemininf  11760  xrminmax  11791  xrlemininf  11797  modremain  12455  nnwosdc  12575  nn0seqcvgd  12578  divgcdcoprm0  12638  ismgmid  13425  grpsubeq0  13634  grpsubadd  13636  eqg0el  13781  isunitd  14085  lsslss  14360  isridlrng  14461  zndvds  14628  znleval  14632  isxmet2d  15037  xblss2  15094  neibl  15180  ellimc3apf  15349  logbgt0b  15655  lgsne0  15732  lgsabs1  15733  lgsquadlem1  15771  m1lgs  15779  iswomninnlem  16477