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  5101  dmfco  5649  omp1eomlem  7198  ltanqg  7515  genpassl  7639  genpassu  7640  ltexprlemloc  7722  caucvgprlemcanl  7759  cauappcvgprlemladdrl  7772  caucvgprlemladdrl  7793  caucvgprprlemaddq  7823  apneg  8686  lemuldiv  8956  msq11  8977  negiso  9030  avglt2  9279  xleaddadd  10011  iooshf  10076  qtri3or  10385  sq11ap  10854  hashen  10931  fihashdom  10950  cjap  11250  sqrt11ap  11382  mingeb  11586  xrnegiso  11606  clim2c  11628  climabs0  11651  absefib  12115  efieq1re  12116  nndivides  12141  oddnn02np1  12224  oddge22np1  12225  evennn02n  12226  evennn2n  12227  halfleoddlt  12238  pc2dvds  12686  pcmpt  12699  issubm  13337  cnntr  14730  cndis  14746  cnpdis  14747  lmres  14753  txhmeo  14824  blininf  14929  cncfmet  15097