Theorem 3bitr4rd 220

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 190	. 2 |- ( ph -> ( ta <-> ps ) )
4		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
5	3, 4	bitr4d 190	1 |- ( ph -> ( ta <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  inimasn  5021  dmfco  5554  omp1eomlem  7059  ltanqg  7341  genpassl  7465  genpassu  7466  ltexprlemloc  7548  caucvgprlemcanl  7585  cauappcvgprlemladdrl  7598  caucvgprlemladdrl  7619  caucvgprprlemaddq  7649  apneg  8509  lemuldiv  8776  msq11  8797  negiso  8850  avglt2  9096  xleaddadd  9823  iooshf  9888  qtri3or  10178  sq11ap  10622  hashen  10697  fihashdom  10716  cjap  10848  sqrt11ap  10980  mingeb  11183  xrnegiso  11203  clim2c  11225  climabs0  11248  absefib  11711  efieq1re  11712  nndivides  11737  oddnn02np1  11817  oddge22np1  11818  evennn02n  11819  evennn2n  11820  halfleoddlt  11831  pc2dvds  12261  pcmpt  12273  cnntr  12865  cndis  12881  cnpdis  12882  lmres  12888  txhmeo  12959  blininf  13064  cncfmet  13219