Theorem 3bitr4rd 219

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr4d.1	|- ( ph -> ( ps <-> ch ) )
3bitr4d.2	|- ( ph -> ( th <-> ps ) )
3bitr4d.3	|- ( ph -> ( ta <-> ch ) )

Assertion

Ref	Expression
3bitr4rd	|- ( ph -> ( ta <-> th ) )

Proof of Theorem 3bitr4rd

Step	Hyp	Ref	Expression
1		3bitr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
2		3bitr4d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	bitr4d 189	. 2 |- ( ph -> ( ta <-> ps ) )
4		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
5	3, 4	bitr4d 189	1 |- ( ph -> ( ta <-> th ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  inimasn  4761  dmfco  5262  ltanqg  6590  genpassl  6714  genpassu  6715  ltexprlemloc  6797  caucvgprlemcanl  6834  cauappcvgprlemladdrl  6847  caucvgprlemladdrl  6868  caucvgprprlemaddq  6898  apneg  7711  lemuldiv  7959  msq11  7980  negiso  8033  avglt2  8270  iooshf  8975  qtri3or  9252  sq11ap  9639  cjap  9793  sqrt11ap  9924  clim2c  10123  climabs0  10146  nndivides  10202  oddnn02np1  10280  oddge22np1  10281  evennn02n  10282  evennn2n  10283  halfleoddlt  10294