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  2830  frecsuclem  6571  indpi  7561  cauappcvgprlemladdru  7875  prsrlt  8006  lesub2  8636  ltsub2  8638  rec11ap  8889  avglt1  9382  rpnegap  9920  modqmuladdnn0  10629  expap0  10830  swrdspsleq  11247  2shfti  11391  mulreap  11424  minmax  11790  lemininf  11794  xrminmax  11825  xrlemininf  11831  modremain  12489  nnwosdc  12609  nn0seqcvgd  12612  divgcdcoprm0  12672  ismgmid  13459  grpsubeq0  13668  grpsubadd  13670  eqg0el  13815  isunitd  14119  lsslss  14394  isridlrng  14495  zndvds  14662  znleval  14666  isxmet2d  15071  xblss2  15128  neibl  15214  ellimc3apf  15383  logbgt0b  15689  lgsne0  15766  lgsabs1  15767  lgsquadlem1  15805  m1lgs  15813  eupth2lem2dc  16309  iswomninnlem  16653