Theorem 3bitr4rd 220

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr4d.1	|- ( ph -> ( ps <-> ch ) )
3bitr4d.2	|- ( ph -> ( th <-> ps ) )
3bitr4d.3	|- ( ph -> ( ta <-> ch ) )

Assertion

Ref	Expression
3bitr4rd	|- ( ph -> ( ta <-> th ) )

Proof of Theorem 3bitr4rd

Step	Hyp	Ref	Expression
1		3bitr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
2		3bitr4d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	bitr4d 190	. 2 |- ( ph -> ( ta <-> ps ) )
4		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
5	3, 4	bitr4d 190	1 |- ( ph -> ( ta <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  inimasn  4956  dmfco  5489  omp1eomlem  6979  ltanqg  7208  genpassl  7332  genpassu  7333  ltexprlemloc  7415  caucvgprlemcanl  7452  cauappcvgprlemladdrl  7465  caucvgprlemladdrl  7486  caucvgprprlemaddq  7516  apneg  8373  lemuldiv  8639  msq11  8660  negiso  8713  avglt2  8959  xleaddadd  9670  iooshf  9735  qtri3or  10020  sq11ap  10458  hashen  10530  fihashdom  10549  cjap  10678  sqrt11ap  10810  xrnegiso  11031  clim2c  11053  climabs0  11076  absefib  11477  efieq1re  11478  nndivides  11500  oddnn02np1  11577  oddge22np1  11578  evennn02n  11579  evennn2n  11580  halfleoddlt  11591  cnntr  12394  cndis  12410  cnpdis  12411  lmres  12417  txhmeo  12488  blininf  12593  cncfmet  12748