Theorem syl5rbb 592

Description: A syllogism inference from two biconditionals.

Hypotheses

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

Assertion

Ref	Expression
syl5rbb	|- (ph -> (ch <-> th))

Proof of Theorem syl5rbb

Step	Hyp	Ref	Expression
1		syl5rbb.1	. . 3 |- (ph -> (ps <-> ch))
2		syl5rbb.2	. . 3 |- (th <-> ps)
3	1, 2	syl5bb 591	. 2 |- (ph -> (th <-> ch))
4	3	bicomd 580	1 |- (ph -> (ch <-> th))

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

This theorem is referenced by:  syl5rbbr 594  sbc8gOLD 2478  sbcralt 2527  sbcralgf 2529  fnresdisj 4523  f1oiso 4881  rdglim2 5157  1idpr 6285  infmsup 7277  fzsuc 7678  fz1sbc 7696  isph 9822  alexsub 15441  cvrnbtwn2 16992  cvrnbtwn4 16996  pmapjat 17314

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