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  5087  dmfco  5629  omp1eomlem  7160  ltanqg  7467  genpassl  7591  genpassu  7592  ltexprlemloc  7674  caucvgprlemcanl  7711  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  caucvgprprlemaddq  7775  apneg  8638  lemuldiv  8908  msq11  8929  negiso  8982  avglt2  9231  xleaddadd  9962  iooshf  10027  qtri3or  10330  sq11ap  10799  hashen  10876  fihashdom  10895  cjap  11071  sqrt11ap  11203  mingeb  11407  xrnegiso  11427  clim2c  11449  climabs0  11472  absefib  11936  efieq1re  11937  nndivides  11962  oddnn02np1  12045  oddge22np1  12046  evennn02n  12047  evennn2n  12048  halfleoddlt  12059  pc2dvds  12499  pcmpt  12512  issubm  13104  cnntr  14461  cndis  14477  cnpdis  14478  lmres  14484  txhmeo  14555  blininf  14660  cncfmet  14828