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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  inimasn  5208  dmfco  5776  omp1eomlem  7440  ltanqg  7773  genpassl  7897  genpassu  7898  ltexprlemloc  7980  caucvgprlemcanl  8017  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgprprlemaddq  8081  apneg  8947  lemuldiv  9219  msq11  9240  negiso  9293  avglt2  9556  xleaddadd  10305  iooshf  10370  qtri3or  10691  sq11ap  11165  hashen  11244  fihashdom  11264  cjap  11693  sqrt11ap  11825  mingeb  12032  xrnegiso  12052  clim2c  12074  climabs0  12097  absefib  12562  efieq1re  12563  nndivides  12588  oddnn02np1  12671  oddge22np1  12672  evennn02n  12673  evennn2n  12674  halfleoddlt  12685  pc2dvds  13137  pcmpt  13150  issubm  13837  cnntr  15468  cndis  15484  cnpdis  15485  lmres  15491  txhmeo  15562  blininf  15667  cncfmet  15835  bposlem1  16328