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  5119  dmfco  5670  omp1eomlem  7222  ltanqg  7548  genpassl  7672  genpassu  7673  ltexprlemloc  7755  caucvgprlemcanl  7792  cauappcvgprlemladdrl  7805  caucvgprlemladdrl  7826  caucvgprprlemaddq  7856  apneg  8719  lemuldiv  8989  msq11  9010  negiso  9063  avglt2  9312  xleaddadd  10044  iooshf  10109  qtri3or  10420  sq11ap  10889  hashen  10966  fihashdom  10985  cjap  11332  sqrt11ap  11464  mingeb  11668  xrnegiso  11688  clim2c  11710  climabs0  11733  absefib  12197  efieq1re  12198  nndivides  12223  oddnn02np1  12306  oddge22np1  12307  evennn02n  12308  evennn2n  12309  halfleoddlt  12320  pc2dvds  12768  pcmpt  12781  issubm  13419  cnntr  14812  cndis  14828  cnpdis  14829  lmres  14835  txhmeo  14906  blininf  15011  cncfmet  15179