Theorem 3bitr3d 548

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 530	. 2 |- (ph -> (th <-> ch))
4		3bitr3d.3	. 2 |- (ph -> (ch <-> ta))
5	3, 4	bitrd 528	1 |- (ph -> (th <-> ta))

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

This theorem is referenced by:  biass 744  sbcel1gv 1980  sbcel2gv 1981  sbcralt 1990  sbcralgf 1992  csbcomg 2017  sbccsb2g 2023  sbcbrg 2662  ordsucun 3082  cbvfo 3885  eloprabg 4007  prlem936a 5153  subcant 5412  conjmult 5797  negeq0t 5806  rebtwnz 6222  flltt 6234  lenegsqt 6885  efcltlem1 7304  cnmet 7904  nmounbi 8439  ip2eqi 8517  minveceu 8583  hvmulcan2t 8940  hvsubcan2t 8942  hi2eqt 8971  fh2t 9562  riesz4 9996  cvbr3 10294  elo 10444  1ded 10671

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