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  5028  dmfco  5564  omp1eomlem  7071  ltanqg  7362  genpassl  7486  genpassu  7487  ltexprlemloc  7569  caucvgprlemcanl  7606  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  caucvgprprlemaddq  7670  apneg  8530  lemuldiv  8797  msq11  8818  negiso  8871  avglt2  9117  xleaddadd  9844  iooshf  9909  qtri3or  10199  sq11ap  10643  hashen  10718  fihashdom  10738  cjap  10870  sqrt11ap  11002  mingeb  11205  xrnegiso  11225  clim2c  11247  climabs0  11270  absefib  11733  efieq1re  11734  nndivides  11759  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  halfleoddlt  11853  pc2dvds  12283  pcmpt  12295  issubm  12695  cnntr  13019  cndis  13035  cnpdis  13036  lmres  13042  txhmeo  13113  blininf  13218  cncfmet  13373