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  5100  dmfco  5647  omp1eomlem  7196  ltanqg  7513  genpassl  7637  genpassu  7638  ltexprlemloc  7720  caucvgprlemcanl  7757  cauappcvgprlemladdrl  7770  caucvgprlemladdrl  7791  caucvgprprlemaddq  7821  apneg  8684  lemuldiv  8954  msq11  8975  negiso  9028  avglt2  9277  xleaddadd  10009  iooshf  10074  qtri3or  10383  sq11ap  10852  hashen  10929  fihashdom  10948  cjap  11217  sqrt11ap  11349  mingeb  11553  xrnegiso  11573  clim2c  11595  climabs0  11618  absefib  12082  efieq1re  12083  nndivides  12108  oddnn02np1  12191  oddge22np1  12192  evennn02n  12193  evennn2n  12194  halfleoddlt  12205  pc2dvds  12653  pcmpt  12666  issubm  13304  cnntr  14697  cndis  14713  cnpdis  14714  lmres  14720  txhmeo  14791  blininf  14896  cncfmet  15064