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  2799  frecsuclem  6492  indpi  7455  cauappcvgprlemladdru  7769  prsrlt  7900  lesub2  8530  ltsub2  8532  rec11ap  8783  avglt1  9276  rpnegap  9808  modqmuladdnn0  10513  expap0  10714  swrdspsleq  11120  2shfti  11142  mulreap  11175  minmax  11541  lemininf  11545  xrminmax  11576  xrlemininf  11582  modremain  12240  nnwosdc  12360  nn0seqcvgd  12363  divgcdcoprm0  12423  ismgmid  13209  grpsubeq0  13418  grpsubadd  13420  eqg0el  13565  isunitd  13868  lsslss  14143  isridlrng  14244  zndvds  14411  znleval  14415  isxmet2d  14820  xblss2  14877  neibl  14963  ellimc3apf  15132  logbgt0b  15438  lgsne0  15515  lgsabs1  15516  lgsquadlem1  15554  m1lgs  15562  iswomninnlem  15988