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  11113  mulreap  11146  minmax  11512  lemininf  11516  xrminmax  11547  xrlemininf  11553  modremain  12211  nnwosdc  12331  nn0seqcvgd  12334  divgcdcoprm0  12394  ismgmid  13180  grpsubeq0  13389  grpsubadd  13391  eqg0el  13536  isunitd  13839  lsslss  14114  isridlrng  14215  zndvds  14382  znleval  14386  isxmet2d  14791  xblss2  14848  neibl  14934  ellimc3apf  15103  logbgt0b  15409  lgsne0  15486  lgsabs1  15487  lgsquadlem1  15525  m1lgs  15533  iswomninnlem  15950