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  5161  dmfco  5723  omp1eomlem  7353  ltanqg  7680  genpassl  7804  genpassu  7805  ltexprlemloc  7887  caucvgprlemcanl  7924  cauappcvgprlemladdrl  7937  caucvgprlemladdrl  7958  caucvgprprlemaddq  7988  apneg  8850  lemuldiv  9120  msq11  9141  negiso  9194  avglt2  9443  xleaddadd  10183  iooshf  10248  qtri3or  10563  sq11ap  11032  hashen  11109  fihashdom  11129  cjap  11546  sqrt11ap  11678  mingeb  11882  xrnegiso  11902  clim2c  11924  climabs0  11947  absefib  12412  efieq1re  12413  nndivides  12438  oddnn02np1  12521  oddge22np1  12522  evennn02n  12523  evennn2n  12524  halfleoddlt  12535  pc2dvds  12983  pcmpt  12996  issubm  13635  cnntr  15036  cndis  15052  cnpdis  15053  lmres  15059  txhmeo  15130  blininf  15235  cncfmet  15403