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  6682  mapsnend  7105  indpi  7715  cauappcvgprlemladdru  8029  prsrlt  8160  lesub2  8792  ltsub2  8794  rec11ap  9048  avglt1  9555  rpnegap  10103  modqmuladdnn0  10825  expap0  11026  hashf1lem1  11306  swrdspsleq  11460  2shfti  11617  mulreap  11650  minmax  12019  lemininf  12023  xrminmax  12055  xrlemininf  12061  modremain  12720  nnwosdc  12840  nn0seqcvgd  12843  divgcdcoprm0  12903  ballotfilemsima  13316  ismgmid  13755  grpsubeq0  13949  grpsubadd  13951  eqg0el  14090  isunitd  14521  lsslss  14826  isridlrng  14927  zndvds  15092  znleval  15096  isxmet2d  15591  xblss2  15648  neibl  15734  ellimc3apf  15903  logbgt0b  16219  prmefexple  16325  bposlem7  16334  lgsne0  16379  lgsabs1  16380  lgsquadlem1  16418  m1lgs  16426  eupth2lem2dc  16922  eupth2lem3lem4fi  16936  iswomninnlem  17323