Theorem syl5rbbr 533

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

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

This theorem is referenced by:  sbco3 1252  sbal2 1351  elabgt 1886  fnrnfv 3744  fressnfv 3823  eluniima 3852  aceq6b 4714  alephnbtwn2 4841  alephval2 4874  1idpr 5105  leloet 5491  xrleloet 5530  muleqaddt 5669  lerec 5828  nn0subt 6108  fzrevt 6443  cjne0t 6766  lenegsqt 6823  metcn4 7905  mdsl2 10157  ghomfo 10296  hmph 10411

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