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  5146  dmfco  5702  omp1eomlem  7261  ltanqg  7587  genpassl  7711  genpassu  7712  ltexprlemloc  7794  caucvgprlemcanl  7831  cauappcvgprlemladdrl  7844  caucvgprlemladdrl  7865  caucvgprprlemaddq  7895  apneg  8758  lemuldiv  9028  msq11  9049  negiso  9102  avglt2  9351  xleaddadd  10083  iooshf  10148  qtri3or  10460  sq11ap  10929  hashen  11006  fihashdom  11025  cjap  11417  sqrt11ap  11549  mingeb  11753  xrnegiso  11773  clim2c  11795  climabs0  11818  absefib  12282  efieq1re  12283  nndivides  12308  oddnn02np1  12391  oddge22np1  12392  evennn02n  12393  evennn2n  12394  halfleoddlt  12405  pc2dvds  12853  pcmpt  12866  issubm  13505  cnntr  14899  cndis  14915  cnpdis  14916  lmres  14922  txhmeo  14993  blininf  15098  cncfmet  15266