Theorem syl5rbbr 535

Description: A syllogism inference from two biconditionals.

Hypotheses

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

Assertion

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

Proof of Theorem syl5rbbr

Step	Hyp	Ref	Expression
1		syl5rbbr.1	. 2 |- (ph -> (ps <-> ch))
2		syl5rbbr.2	. . 3 |- (ps <-> th)
3	2	bicomi 172	. 2 |- (th <-> ps)
4	1, 3	syl5rbb 533	1 |- (ph -> (ch <-> th))

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

This theorem is referenced by:  sbco3 1257  sbal2 1358  elabgt 1895  fnrnfv 3759  fressnfv 3838  eluniima 3867  aceq6b 4742  alephnbtwn2 4869  alephval2 4902  1idpr 5133  leloet 5518  xrleloet 5557  muleqaddt 5700  lerec 5880  nn0subt 6161  fzrevt 6511  cjne0t 6831  lenegsqt 6885  metcn4 7971  mdsl2 10249  ghomfo 10391  hmph 10524

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