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  2766  frecsuclem  6410  indpi  7344  cauappcvgprlemladdru  7658  prsrlt  7789  lesub2  8417  ltsub2  8419  rec11ap  8670  avglt1  9160  rpnegap  9689  modqmuladdnn0  10371  expap0  10553  2shfti  10843  mulreap  10876  minmax  11241  lemininf  11245  xrminmax  11276  xrlemininf  11282  modremain  11937  nn0seqcvgd  12044  divgcdcoprm0  12104  ismgmid  12802  grpsubeq0  12962  grpsubadd  12964  isunitd  13281  lsslss  13474  isxmet2d  13988  xblss2  14045  neibl  14131  ellimc3apf  14269  logbgt0b  14524  lgsne0  14579  lgsabs1  14580  m1lgs  14592  iswomninnlem  14937