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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ceqsralt  2849  frecsuclem  6681  mapsnend  7103  indpi  7715  cauappcvgprlemladdru  8029  prsrlt  8160  lesub2  8792  ltsub2  8794  rec11ap  9048  avglt1  9555  rpnegap  10104  modqmuladdnn0  10826  expap0  11027  hashf1lem1  11307  swrdspsleq  11461  2shfti  11618  mulreap  11651  minmax  12020  lemininf  12024  xrminmax  12056  xrlemininf  12062  modremain  12721  nnwosdc  12841  nn0seqcvgd  12844  divgcdcoprm0  12904  ballotfilemsima  13317  ismgmid  13756  grpsubeq0  13950  grpsubadd  13952  eqg0el  14091  isunitd  14522  lsslss  14827  isridlrng  14928  zndvds  15093  znleval  15097  isxmet2d  15574  xblss2  15631  neibl  15717  ellimc3apf  15886  logbgt0b  16202  prmefexple  16308  bposlem7  16317  lgsne0  16362  lgsabs1  16363  lgsquadlem1  16401  m1lgs  16409  eupth2lem2dc  16905  eupth2lem3lem4fi  16919  iswomninnlem  17306