Theorem 3bitrd 544

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

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

This theorem is referenced by:  sbc3ang 1979  sbcgf 1986  sbccomglem 1988  sbccomg 1989  sbcabel 1996  sbcel12g 2011  sbcnestg 2038  dedth3v 2385  dedth4v 2386  elimhyp3v 2392  elimhyp4v 2393  keephyp3v 2398  sbcbrg 2662  unfilem3 4550  r1pwcl 4687  lesub2t 5661  ltsub2t 5663  suble0t 5675  ltdiv23t 5892  lediv23t 5893  supxrbnd1 6095  supxrbnd2 6096  fzshftralt 6522  iserzshft 7144  islp2 7747  neibl 7877  metcnp 7887  metcn 7889  metcn4 7971  imsmetlem 8323  ipz 8372  minveclem24 8568  minveclem27 8571  hvmulcant 8939  hvsubcant 8941  hoeq2t 9757  leoptrit 10069  atcv0eq 10306  ismona 10737  imonclem 10741  isepia 10747

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