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  2801  frecsuclem  6510  indpi  7485  cauappcvgprlemladdru  7799  prsrlt  7930  lesub2  8560  ltsub2  8562  rec11ap  8813  avglt1  9306  rpnegap  9838  modqmuladdnn0  10545  expap0  10746  swrdspsleq  11153  2shfti  11227  mulreap  11260  minmax  11626  lemininf  11630  xrminmax  11661  xrlemininf  11667  modremain  12325  nnwosdc  12445  nn0seqcvgd  12448  divgcdcoprm0  12508  ismgmid  13294  grpsubeq0  13503  grpsubadd  13505  eqg0el  13650  isunitd  13953  lsslss  14228  isridlrng  14329  zndvds  14496  znleval  14500  isxmet2d  14905  xblss2  14962  neibl  15048  ellimc3apf  15217  logbgt0b  15523  lgsne0  15600  lgsabs1  15601  lgsquadlem1  15639  m1lgs  15647  iswomninnlem  16160