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  8785  ltsub2  8787  rec11ap  9040  avglt1  9544  rpnegap  10087  modqmuladdnn0  10805  expap0  11006  hashf1lem1  11285  swrdspsleq  11439  2shfti  11596  mulreap  11629  minmax  11996  lemininf  12000  xrminmax  12031  xrlemininf  12037  modremain  12696  nnwosdc  12816  nn0seqcvgd  12819  divgcdcoprm0  12879  ballotfilemsima  13259  ismgmid  13697  grpsubeq0  13891  grpsubadd  13893  eqg0el  14032  isunitd  14413  lsslss  14718  isridlrng  14819  zndvds  14984  znleval  14988  isxmet2d  15449  xblss2  15506  neibl  15592  ellimc3apf  15761  logbgt0b  16068  lgsne0  16157  lgsabs1  16158  lgsquadlem1  16196  m1lgs  16204  eupth2lem2dc  16700  eupth2lem3lem4fi  16714  iswomninnlem  17099