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  5149  dmfco  5707  omp1eomlem  7277  ltanqg  7603  genpassl  7727  genpassu  7728  ltexprlemloc  7810  caucvgprlemcanl  7847  cauappcvgprlemladdrl  7860  caucvgprlemladdrl  7881  caucvgprprlemaddq  7911  apneg  8774  lemuldiv  9044  msq11  9065  negiso  9118  avglt2  9367  xleaddadd  10100  iooshf  10165  qtri3or  10477  sq11ap  10946  hashen  11023  fihashdom  11042  cjap  11438  sqrt11ap  11570  mingeb  11774  xrnegiso  11794  clim2c  11816  climabs0  11839  absefib  12303  efieq1re  12304  nndivides  12329  oddnn02np1  12412  oddge22np1  12413  evennn02n  12414  evennn2n  12415  halfleoddlt  12426  pc2dvds  12874  pcmpt  12887  issubm  13526  cnntr  14920  cndis  14936  cnpdis  14937  lmres  14943  txhmeo  15014  blininf  15119  cncfmet  15287