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  5088  dmfco  5630  omp1eomlem  7161  ltanqg  7469  genpassl  7593  genpassu  7594  ltexprlemloc  7676  caucvgprlemcanl  7713  cauappcvgprlemladdrl  7726  caucvgprlemladdrl  7747  caucvgprprlemaddq  7777  apneg  8640  lemuldiv  8910  msq11  8931  negiso  8984  avglt2  9233  xleaddadd  9964  iooshf  10029  qtri3or  10332  sq11ap  10801  hashen  10878  fihashdom  10897  cjap  11073  sqrt11ap  11205  mingeb  11409  xrnegiso  11429  clim2c  11451  climabs0  11474  absefib  11938  efieq1re  11939  nndivides  11964  oddnn02np1  12047  oddge22np1  12048  evennn02n  12049  evennn2n  12050  halfleoddlt  12061  pc2dvds  12509  pcmpt  12522  issubm  13114  cnntr  14471  cndis  14487  cnpdis  14488  lmres  14494  txhmeo  14565  blininf  14670  cncfmet  14838