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  2828  frecsuclem  6567  indpi  7552  cauappcvgprlemladdru  7866  prsrlt  7997  lesub2  8627  ltsub2  8629  rec11ap  8880  avglt1  9373  rpnegap  9911  modqmuladdnn0  10620  expap0  10821  swrdspsleq  11238  2shfti  11382  mulreap  11415  minmax  11781  lemininf  11785  xrminmax  11816  xrlemininf  11822  modremain  12480  nnwosdc  12600  nn0seqcvgd  12603  divgcdcoprm0  12663  ismgmid  13450  grpsubeq0  13659  grpsubadd  13661  eqg0el  13806  isunitd  14110  lsslss  14385  isridlrng  14486  zndvds  14653  znleval  14657  isxmet2d  15062  xblss2  15119  neibl  15205  ellimc3apf  15374  logbgt0b  15680  lgsne0  15757  lgsabs1  15758  lgsquadlem1  15796  m1lgs  15804  iswomninnlem  16589