Theorem syl5rbbr 537

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 535	1 |- (ph -> (ch <-> th))

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

This theorem is referenced by:  sbco3 1259  sbal2 1360  elabgt 1898  fnrnfv 3765  fressnfv 3844  eluniima 3873  aceq6b 4752  alephnbtwn2 4880  alephval2 4913  1idpr 5145  leloet 5530  xrleloet 5569  muleqaddt 5712  lerec 5882  nn0subt 6163  fzrevt 6512  cjne0t 6831  lenegsqt 6885  metcn4 7968  mdsl2 10244  ghomfo 10386  hmph 10510

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