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  2831  frecsuclem  6615  indpi  7605  cauappcvgprlemladdru  7919  prsrlt  8050  lesub2  8679  ltsub2  8681  rec11ap  8932  avglt1  9425  rpnegap  9965  modqmuladdnn0  10676  expap0  10877  swrdspsleq  11297  2shfti  11454  mulreap  11487  minmax  11853  lemininf  11857  xrminmax  11888  xrlemininf  11894  modremain  12553  nnwosdc  12673  nn0seqcvgd  12676  divgcdcoprm0  12736  ismgmid  13523  grpsubeq0  13732  grpsubadd  13734  eqg0el  13879  isunitd  14184  lsslss  14460  isridlrng  14561  zndvds  14728  znleval  14732  isxmet2d  15142  xblss2  15199  neibl  15285  ellimc3apf  15454  logbgt0b  15760  lgsne0  15840  lgsabs1  15841  lgsquadlem1  15879  m1lgs  15887  eupth2lem2dc  16383  eupth2lem3lem4fi  16397  iswomninnlem  16765