Theorem syl6rbb 537

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 536	. 2 |- (ph -> (ps <-> th))
4	3	bicomd 521	1 |- (ph -> (th <-> ps))

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

This theorem is referenced by:  syl6rbbr 539  necon4bid 1630  resopab2 3398  funconstss 3808  2ndconst 4097  xpopth 4106  brdom7disj 4804  alephval2 4902  negeq0t 5806  infmsup 6068  supxrre 6083  supxrbnd1 6095  supxrbnd2 6096  elznn0 6149  dfuz 6202  0top 7635  islp2 7747  nmo0 8451  sincosq3sgn 8706  sincosq4sgn 8707  leop3t 10058  leoptrit 10069  dtopcl 10615

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