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  2790  frecsuclem  6464  indpi  7409  cauappcvgprlemladdru  7723  prsrlt  7854  lesub2  8484  ltsub2  8486  rec11ap  8737  avglt1  9230  rpnegap  9761  modqmuladdnn0  10460  expap0  10661  2shfti  10996  mulreap  11029  minmax  11395  lemininf  11399  xrminmax  11430  xrlemininf  11436  modremain  12094  nnwosdc  12206  nn0seqcvgd  12209  divgcdcoprm0  12269  ismgmid  13020  grpsubeq0  13218  grpsubadd  13220  eqg0el  13359  isunitd  13662  lsslss  13937  isridlrng  14038  zndvds  14205  znleval  14209  isxmet2d  14584  xblss2  14641  neibl  14727  ellimc3apf  14896  logbgt0b  15202  lgsne0  15279  lgsabs1  15280  lgsquadlem1  15318  m1lgs  15326  iswomninnlem  15693