Theorem 3bitr3d 546

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula.

Hypotheses

Ref	Expression
3bitr3d.1	|- (ph -> (ps <-> ch))
3bitr3d.2	|- (ph -> (ps <-> th))
3bitr3d.3	|- (ph -> (ch <-> ta))

Assertion

Ref	Expression
3bitr3d	|- (ph -> (th <-> ta))

Proof of Theorem 3bitr3d

Step	Hyp	Ref	Expression
1		3bitr3d.2	. . 3 |- (ph -> (ps <-> th))
2		3bitr3d.1	. . 3 |- (ph -> (ps <-> ch))
3	1, 2	bitr3d 528	. 2 |- (ph -> (th <-> ch))
4		3bitr3d.3	. 2 |- (ph -> (ch <-> ta))
5	3, 4	bitrd 526	1 |- (ph -> (th <-> ta))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  biass 742  sbcel1gv 1970  sbcel2gv 1971  sbcralt 1980  sbcralgf 1982  csbcomg 2007  sbccsb2g 2013  sbcbrg 2652  ordsucun 3072  cbvfo 3870  eloprabg 3992  prlem936a 5125  subcant 5384  conjmult 5753  negeq0t 5762  rebtwnz 6170  flltt 6179  lenegsqt 6823  efcltlem1 7246  cnmet 7843  nmounbi 8371  ip2eqi 8448  minveceu 8514  hvmulcan2t 8861  hvsubcan2t 8863  hi2eqt 8892  fh2t 9479  riesz4 9911  cvbr3 10202  elo 10345  1ded 10515

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain