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  5058  dmfco  5597  omp1eomlem  7107  ltanqg  7413  genpassl  7537  genpassu  7538  ltexprlemloc  7620  caucvgprlemcanl  7657  cauappcvgprlemladdrl  7670  caucvgprlemladdrl  7691  caucvgprprlemaddq  7721  apneg  8582  lemuldiv  8852  msq11  8873  negiso  8926  avglt2  9172  xleaddadd  9901  iooshf  9966  qtri3or  10257  sq11ap  10702  hashen  10778  fihashdom  10797  cjap  10929  sqrt11ap  11061  mingeb  11264  xrnegiso  11284  clim2c  11306  climabs0  11329  absefib  11792  efieq1re  11793  nndivides  11818  oddnn02np1  11899  oddge22np1  11900  evennn02n  11901  evennn2n  11902  halfleoddlt  11913  pc2dvds  12343  pcmpt  12355  issubm  12885  cnntr  14021  cndis  14037  cnpdis  14038  lmres  14044  txhmeo  14115  blininf  14220  cncfmet  14375