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  2798  frecsuclem  6491  indpi  7454  cauappcvgprlemladdru  7768  prsrlt  7899  lesub2  8529  ltsub2  8531  rec11ap  8782  avglt1  9275  rpnegap  9807  modqmuladdnn0  10511  expap0  10712  2shfti  11084  mulreap  11117  minmax  11483  lemininf  11487  xrminmax  11518  xrlemininf  11524  modremain  12182  nnwosdc  12302  nn0seqcvgd  12305  divgcdcoprm0  12365  ismgmid  13151  grpsubeq0  13360  grpsubadd  13362  eqg0el  13507  isunitd  13810  lsslss  14085  isridlrng  14186  zndvds  14353  znleval  14357  isxmet2d  14762  xblss2  14819  neibl  14905  ellimc3apf  15074  logbgt0b  15380  lgsne0  15457  lgsabs1  15458  lgsquadlem1  15496  m1lgs  15504  iswomninnlem  15921