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  5185  dmfco  5750  omp1eomlem  7398  ltanqg  7731  genpassl  7855  genpassu  7856  ltexprlemloc  7938  caucvgprlemcanl  7975  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgprprlemaddq  8039  apneg  8902  lemuldiv  9172  msq11  9193  negiso  9246  avglt2  9495  xleaddadd  10239  iooshf  10304  qtri3or  10624  sq11ap  11094  hashen  11172  fihashdom  11192  cjap  11616  sqrt11ap  11748  mingeb  11952  xrnegiso  11972  clim2c  11994  climabs0  12017  absefib  12482  efieq1re  12483  nndivides  12508  oddnn02np1  12591  oddge22np1  12592  evennn02n  12593  evennn2n  12594  halfleoddlt  12605  pc2dvds  13053  pcmpt  13066  issubm  13727  cnntr  15216  cndis  15232  cnpdis  15233  lmres  15239  txhmeo  15310  blininf  15415  cncfmet  15583