Theorem 3bitr4rd 221

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 191	. 2 |- ( ph -> ( ta <-> ps ) )
4		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
5	3, 4	bitr4d 191	1 |- ( ph -> ( ta <-> th ) )

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:  inimasn  5043  dmfco  5581  omp1eomlem  7088  ltanqg  7394  genpassl  7518  genpassu  7519  ltexprlemloc  7601  caucvgprlemcanl  7638  cauappcvgprlemladdrl  7651  caucvgprlemladdrl  7672  caucvgprprlemaddq  7702  apneg  8562  lemuldiv  8832  msq11  8853  negiso  8906  avglt2  9152  xleaddadd  9881  iooshf  9946  qtri3or  10236  sq11ap  10680  hashen  10755  fihashdom  10774  cjap  10906  sqrt11ap  11038  mingeb  11241  xrnegiso  11261  clim2c  11283  climabs0  11306  absefib  11769  efieq1re  11770  nndivides  11795  oddnn02np1  11875  oddge22np1  11876  evennn02n  11877  evennn2n  11878  halfleoddlt  11889  pc2dvds  12319  pcmpt  12331  issubm  12791  cnntr  13507  cndis  13523  cnpdis  13524  lmres  13530  txhmeo  13601  blininf  13706  cncfmet  13861