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  2840  frecsuclem  6636  mapsnend  7051  indpi  7656  cauappcvgprlemladdru  7970  prsrlt  8101  lesub2  8730  ltsub2  8732  rec11ap  8983  avglt1  9476  rpnegap  10018  modqmuladdnn0  10729  expap0  10930  swrdspsleq  11355  2shfti  11512  mulreap  11545  minmax  11911  lemininf  11915  xrminmax  11946  xrlemininf  11952  modremain  12611  nnwosdc  12731  nn0seqcvgd  12734  divgcdcoprm0  12794  ismgmid  13582  grpsubeq0  13791  grpsubadd  13793  eqg0el  13938  isunitd  14243  lsslss  14521  isridlrng  14622  zndvds  14789  znleval  14793  isxmet2d  15205  xblss2  15262  neibl  15348  ellimc3apf  15517  logbgt0b  15823  lgsne0  15903  lgsabs1  15904  lgsquadlem1  15942  m1lgs  15950  eupth2lem2dc  16446  eupth2lem3lem4fi  16460  iswomninnlem  16826