Theorem 3bitrd 546

Description: Deduction from transitivity of biconditional.

Hypotheses

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

Assertion

Ref	Expression
3bitrd	|- (ph -> (ps <-> ta))

Proof of Theorem 3bitrd

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

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

This theorem is referenced by:  sbc3ang 1982  sbcgf 1989  sbccomglem 1991  sbccomg 1992  sbcabel 1999  sbcel12g 2014  sbcnestg 2041  dedth3v 2389  dedth4v 2390  elimhyp3v 2396  elimhyp4v 2397  keephyp3v 2402  sbcbrg 2667  unfilem3 4562  r1pwcl 4697  lesub2t 5673  ltsub2t 5675  suble0t 5687  ltdiv23t 5894  lediv23t 5895  supxrbnd1 6097  supxrbnd2 6098  fzshftralt 6523  iserzshft 7144  islp2 7744  neibl 7874  metcnp 7884  metcn 7886  metcn4 7968  imsmetlem 8319  ipz 8368  minveclem24 8564  minveclem27 8567  hvmulcant 8934  hvsubcant 8936  hoeq2t 9752  leoptrit 10064  atcv0eq 10301  ismona 10708  imonclem 10712  isepia 10718

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