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  2765  frecsuclem  6407  indpi  7341  cauappcvgprlemladdru  7655  prsrlt  7786  lesub2  8414  ltsub2  8416  rec11ap  8667  avglt1  9157  rpnegap  9686  modqmuladdnn0  10368  expap0  10550  2shfti  10840  mulreap  10873  minmax  11238  lemininf  11242  xrminmax  11273  xrlemininf  11279  modremain  11934  nn0seqcvgd  12041  divgcdcoprm0  12101  ismgmid  12796  grpsubeq0  12956  grpsubadd  12958  isunitd  13275  isxmet2d  13851  xblss2  13908  neibl  13994  ellimc3apf  14132  logbgt0b  14387  lgsne0  14442  lgsabs1  14443  m1lgs  14455  iswomninnlem  14800