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  2787  frecsuclem  6459  indpi  7402  cauappcvgprlemladdru  7716  prsrlt  7847  lesub2  8476  ltsub2  8478  rec11ap  8729  avglt1  9221  rpnegap  9752  modqmuladdnn0  10439  expap0  10640  2shfti  10975  mulreap  11008  minmax  11373  lemininf  11377  xrminmax  11408  xrlemininf  11414  modremain  12070  nnwosdc  12176  nn0seqcvgd  12179  divgcdcoprm0  12239  ismgmid  12960  grpsubeq0  13158  grpsubadd  13160  eqg0el  13299  isunitd  13602  lsslss  13877  isridlrng  13978  zndvds  14137  znleval  14141  isxmet2d  14516  xblss2  14573  neibl  14659  ellimc3apf  14814  logbgt0b  15098  lgsne0  15154  lgsabs1  15155  lgsquadlem1  15191  m1lgs  15192  iswomninnlem  15539