Theorem sylan2br 348

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylan.1	|- ((ph /\ ps) -> ch)
sylan2br.2	|- (ps <-> th)

Assertion

Ref	Expression
sylan2br	|- ((ph /\ th) -> ch)

Proof of Theorem sylan2br

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ((ph /\ ps) -> ch)
2		sylan2br.2	. . 3 |- (ps <-> th)
3	2	biimpr 134	. 2 |- (th -> ps)
4	1, 3	sylan2 346	1 |- ((ph /\ th) -> ch)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  syl2anbr 351  po2nr 2135  tfindsg2 2403  imainss 2649  imadif 2714  fnop 2727  tfrlem2 2950  tz7.48-2 2995  aceq5 3563  ac6lem 3575  zornlem7 3609  suppsr 4016  supsrlem6 4024  supre 4054  uzind2 4604  axhis42 5049  hoco 5598

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