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  2841  frecsuclem  6637  mapsnend  7052  indpi  7657  cauappcvgprlemladdru  7971  prsrlt  8102  lesub2  8731  ltsub2  8733  rec11ap  8984  avglt1  9477  rpnegap  10019  modqmuladdnn0  10730  expap0  10931  swrdspsleq  11359  2shfti  11516  mulreap  11549  minmax  11915  lemininf  11919  xrminmax  11950  xrlemininf  11956  modremain  12615  nnwosdc  12735  nn0seqcvgd  12738  divgcdcoprm0  12798  ismgmid  13590  grpsubeq0  13799  grpsubadd  13801  eqg0el  13946  isunitd  14251  lsslss  14529  isridlrng  14630  zndvds  14797  znleval  14801  isxmet2d  15213  xblss2  15270  neibl  15356  ellimc3apf  15525  logbgt0b  15831  lgsne0  15911  lgsabs1  15912  lgsquadlem1  15950  m1lgs  15958  eupth2lem2dc  16454  eupth2lem3lem4fi  16468  iswomninnlem  16834