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  2827  frecsuclem  6550  indpi  7525  cauappcvgprlemladdru  7839  prsrlt  7970  lesub2  8600  ltsub2  8602  rec11ap  8853  avglt1  9346  rpnegap  9878  modqmuladdnn0  10585  expap0  10786  swrdspsleq  11194  2shfti  11337  mulreap  11370  minmax  11736  lemininf  11740  xrminmax  11771  xrlemininf  11777  modremain  12435  nnwosdc  12555  nn0seqcvgd  12558  divgcdcoprm0  12618  ismgmid  13405  grpsubeq0  13614  grpsubadd  13616  eqg0el  13761  isunitd  14064  lsslss  14339  isridlrng  14440  zndvds  14607  znleval  14611  isxmet2d  15016  xblss2  15073  neibl  15159  ellimc3apf  15328  logbgt0b  15634  lgsne0  15711  lgsabs1  15712  lgsquadlem1  15750  m1lgs  15758  iswomninnlem  16376