Theorem syl5ibr 182

Description: A mixed syllogism inference from a nested implication and a biconditional.

Hypotheses

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

Assertion

Ref	Expression
syl5ibr	|- (ph -> (th -> ch))

Proof of Theorem syl5ibr

Step	Hyp	Ref	Expression
1		syl5ibr.1	. 2 |- (ph -> (ps -> ch))
2		syl5ibr.2	. . 3 |- (ps <-> th)
3	2	biimpr 134	. 2 |- (th -> ps)
4	1, 3	syl5 22	1 |- (ph -> (th -> ch))

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

This theorem is referenced by:  ceqex 1410  pssdifn0 1750  wereu 2197  ordelord 2221  findsg 2398  tfindsg 2402  tfindes 2404  tfinds2 2405  ralxp 2456  cotr 2625  cnvsym 2626  funex 2741  funfvopi 2853  funfvima 2904  eceqopreq 3249  th3qlem1 3250  unen 3338  php3 3411  pssnn 3428  isfinite2 3437  sucprcreg 3451  inf3lem2 3465  setind 3492  aceq5lem4 3561  kmlem12 3591  zornlem4 3606  cardlim 3657  arch 4521  crulem 4528  uzwo3lem2 4615  qbtwnre 4650  infmap2lem1 4951  hlimcaui 5141  spanun 5450  spansn 5462  mdbr3 5729  mdbr4 5730  mdsymlem6 5781  sumdmd 5787

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

metamath.org