Theorem 3bitr3d 607

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

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

This theorem is referenced by:  biass 816  sbcel1gvOLD 2511  sbcel2gvOLD 2513  sbcralt 2527  sbcralgf 2529  csbcomg 2560  sbccsb2g 2566  sbcbrgOLD 3391  ordsucun 3905  cbvfo 4861  eloprabg 4936  oeoa 5272  sbc3org 5827  prlem936a 6305  subcan 6572  conjmul 6975  negeq0 6984  rebtwnz 7435  fllt 7473  lenegsq 8137  efcltlem1 8566  cnmet 9182  nmounbi 9778  ip2eqi 9858  minveceu 9928  hvmulcan 10571  hvsubcan2 10575  hi2eq 10604  fh2 11195  riesz4i 11633  cvbr3i 11939  bnj1377 13095  elo 14342  1ded 15085  blssp 15844  isdmn3 16222  sbcne12g 16409  latlem12 16873

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 164  df-an 242

Copyright terms: Public domain