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  2830  frecsuclem  6572  indpi  7562  cauappcvgprlemladdru  7876  prsrlt  8007  lesub2  8637  ltsub2  8639  rec11ap  8890  avglt1  9383  rpnegap  9921  modqmuladdnn0  10631  expap0  10832  swrdspsleq  11252  2shfti  11409  mulreap  11442  minmax  11808  lemininf  11812  xrminmax  11843  xrlemininf  11849  modremain  12508  nnwosdc  12628  nn0seqcvgd  12631  divgcdcoprm0  12691  ismgmid  13478  grpsubeq0  13687  grpsubadd  13689  eqg0el  13834  isunitd  14139  lsslss  14414  isridlrng  14515  zndvds  14682  znleval  14686  isxmet2d  15091  xblss2  15148  neibl  15234  ellimc3apf  15403  logbgt0b  15709  lgsne0  15786  lgsabs1  15787  lgsquadlem1  15825  m1lgs  15833  eupth2lem2dc  16329  eupth2lem3lem4fi  16343  iswomninnlem  16705