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  6677  mapsnend  7099  indpi  7709  cauappcvgprlemladdru  8023  prsrlt  8154  lesub2  8786  ltsub2  8788  rec11ap  9042  avglt1  9548  rpnegap  10097  modqmuladdnn0  10818  expap0  11019  hashf1lem1  11299  swrdspsleq  11453  2shfti  11610  mulreap  11643  minmax  12011  lemininf  12015  xrminmax  12047  xrlemininf  12053  modremain  12712  nnwosdc  12832  nn0seqcvgd  12835  divgcdcoprm0  12895  ballotfilemsima  13308  ismgmid  13746  grpsubeq0  13940  grpsubadd  13942  eqg0el  14081  isunitd  14462  lsslss  14767  isridlrng  14868  zndvds  15033  znleval  15037  isxmet2d  15498  xblss2  15555  neibl  15641  ellimc3apf  15810  logbgt0b  16121  prmefexple  16206  lgsne0  16255  lgsabs1  16256  lgsquadlem1  16294  m1lgs  16302  eupth2lem2dc  16798  eupth2lem3lem4fi  16812  iswomninnlem  17197