Theorem syl5bbr 412

Description: A syllogism inference from two biconditionals.

Hypotheses

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

Assertion

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

Proof of Theorem syl5bbr

Step	Hyp	Ref	Expression
1		syl5bbr.1	. 2 |- (ph -> (ps <-> ch))
2		syl5bbr.2	. . 3 |- (ps <-> th)
3	2	bicomi 150	. 2 |- (th <-> ps)
4	1, 3	syl5bb 410	1 |- (ph -> (th <-> ch))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  3bitr3g 427  sbco2 913  elabf 1414  sbceq1 1443  iunpw 2040  opabsb 2114  opelopabg 2115  dfom2 2374  tfinds 2401  resieq 2581  fneu 2728  dmfco 2864  fvco 2865  brecop 3242  zornlem7 3609  ltpiord 3809  map2psrpr 4014  suppsr 4016  supsrlem6 4024  supre 4054  mul0or 4210  lt2sq 4414  uzind 4603  sqr00t 4770  jplem1 5701  hatomistic 5755

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org