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  5048  dmfco  5586  omp1eomlem  7095  ltanqg  7401  genpassl  7525  genpassu  7526  ltexprlemloc  7608  caucvgprlemcanl  7645  cauappcvgprlemladdrl  7658  caucvgprlemladdrl  7679  caucvgprprlemaddq  7709  apneg  8570  lemuldiv  8840  msq11  8861  negiso  8914  avglt2  9160  xleaddadd  9889  iooshf  9954  qtri3or  10245  sq11ap  10690  hashen  10766  fihashdom  10785  cjap  10917  sqrt11ap  11049  mingeb  11252  xrnegiso  11272  clim2c  11294  climabs0  11317  absefib  11780  efieq1re  11781  nndivides  11806  oddnn02np1  11887  oddge22np1  11888  evennn02n  11889  evennn2n  11890  halfleoddlt  11901  pc2dvds  12331  pcmpt  12343  issubm  12868  cnntr  13764  cndis  13780  cnpdis  13781  lmres  13787  txhmeo  13858  blininf  13963  cncfmet  14118