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  5084  dmfco  5626  omp1eomlem  7155  ltanqg  7462  genpassl  7586  genpassu  7587  ltexprlemloc  7669  caucvgprlemcanl  7706  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  caucvgprprlemaddq  7770  apneg  8632  lemuldiv  8902  msq11  8923  negiso  8976  avglt2  9225  xleaddadd  9956  iooshf  10021  qtri3or  10313  sq11ap  10781  hashen  10858  fihashdom  10877  cjap  11053  sqrt11ap  11185  mingeb  11388  xrnegiso  11408  clim2c  11430  climabs0  11453  absefib  11917  efieq1re  11918  nndivides  11943  oddnn02np1  12024  oddge22np1  12025  evennn02n  12026  evennn2n  12027  halfleoddlt  12038  pc2dvds  12471  pcmpt  12484  issubm  13047  cnntr  14404  cndis  14420  cnpdis  14421  lmres  14427  txhmeo  14498  blininf  14603  cncfmet  14771