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  2849  frecsuclem  6667  mapsnend  7089  indpi  7699  cauappcvgprlemladdru  8013  prsrlt  8144  lesub2  8775  ltsub2  8777  rec11ap  9030  avglt1  9523  rpnegap  10066  modqmuladdnn0  10783  expap0  10984  hashf1lem1  11263  swrdspsleq  11417  2shfti  11574  mulreap  11607  minmax  11974  lemininf  11978  xrminmax  12009  xrlemininf  12015  modremain  12674  nnwosdc  12794  nn0seqcvgd  12797  divgcdcoprm0  12857  ballotfilemsima  13237  ismgmid  13674  grpsubeq0  13868  grpsubadd  13870  eqg0el  14009  isunitd  14386  lsslss  14690  isridlrng  14791  zndvds  14956  znleval  14960  isxmet2d  15372  xblss2  15429  neibl  15515  ellimc3apf  15684  logbgt0b  15991  lgsne0  16071  lgsabs1  16072  lgsquadlem1  16110  m1lgs  16118  eupth2lem2dc  16614  eupth2lem3lem4fi  16628  iswomninnlem  17004