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  5704  omp1eomlem  7272  ltanqg  7598  genpassl  7722  genpassu  7723  ltexprlemloc  7805  caucvgprlemcanl  7842  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  caucvgprprlemaddq  7906  apneg  8769  lemuldiv  9039  msq11  9060  negiso  9113  avglt2  9362  xleaddadd  10095  iooshf  10160  qtri3or  10472  sq11ap  10941  hashen  11018  fihashdom  11037  cjap  11433  sqrt11ap  11565  mingeb  11769  xrnegiso  11789  clim2c  11811  climabs0  11834  absefib  12298  efieq1re  12299  nndivides  12324  oddnn02np1  12407  oddge22np1  12408  evennn02n  12409  evennn2n  12410  halfleoddlt  12421  pc2dvds  12869  pcmpt  12882  issubm  13521  cnntr  14915  cndis  14931  cnpdis  14932  lmres  14938  txhmeo  15009  blininf  15114  cncfmet  15282