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  5083  dmfco  5625  omp1eomlem  7153  ltanqg  7460  genpassl  7584  genpassu  7585  ltexprlemloc  7667  caucvgprlemcanl  7704  cauappcvgprlemladdrl  7717  caucvgprlemladdrl  7738  caucvgprprlemaddq  7768  apneg  8630  lemuldiv  8900  msq11  8921  negiso  8974  avglt2  9222  xleaddadd  9953  iooshf  10018  qtri3or  10310  sq11ap  10778  hashen  10855  fihashdom  10874  cjap  11050  sqrt11ap  11182  mingeb  11385  xrnegiso  11405  clim2c  11427  climabs0  11450  absefib  11914  efieq1re  11915  nndivides  11940  oddnn02np1  12021  oddge22np1  12022  evennn02n  12023  evennn2n  12024  halfleoddlt  12035  pc2dvds  12468  pcmpt  12481  issubm  13044  cnntr  14393  cndis  14409  cnpdis  14410  lmres  14416  txhmeo  14487  blininf  14592  cncfmet  14747