Theorem syl6rbb 539

Description: A syllogism inference from two biconditionals.

Hypotheses

Ref	Expression
syl6rbb.1	|- (ph -> (ps <-> ch))
syl6rbb.2	|- (ch <-> th)

Assertion

Ref	Expression
syl6rbb	|- (ph -> (th <-> ps))

Proof of Theorem syl6rbb

Step	Hyp	Ref	Expression
1		syl6rbb.1	. . 3 |- (ph -> (ps <-> ch))
2		syl6rbb.2	. . 3 |- (ch <-> th)
3	1, 2	syl6bb 538	. 2 |- (ph -> (ps <-> th))
4	3	bicomd 523	1 |- (ph -> (th <-> ps))

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

This theorem is referenced by:  syl6rbbr 541  necon4bid 1633  resopab2 3404  funconstss 3814  2ndconst 4103  xpopth 4112  brdom7disj 4814  alephval2 4913  negeq0t 5808  infmsup 6070  supxrre 6085  supxrbnd1 6097  supxrbnd2 6098  elznn0 6151  dfuz 6204  0top 7634  islp2 7744  nmo0 8447  sincosq3sgn 8701  sincosq4sgn 8702  leop3t 10053  leoptrit 10064  dtopcl 10586

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