Theorem syl5bir 209

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5bir

Step	Hyp	Ref	Expression
1		syl5bir.1	. . 3 |- (ps <-> ph)
2	1	biimpri 197	. 2 |- (ph -> ps)
3		syl5bir.2	. 2 |- (ch -> (ps -> th))
4	2, 3	syl5 28	1 |- (ch -> (ph -> th))

Syntax hints:   -> wi 4   <-> wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3imtr3g  260  oplem1  930  nic-ax  1438  19.30  1604  19.33b  1608  ax10  1944  necon4bd  2578  ceqex  2969  ssdisj  3600  pssdifn0  3611  ltfintr  4459  evenodddisj  4516  sfinltfin  4535  fun11iun  5305  funopfv  5357  dff3  5420  funfvima  5459  trrd  5925  peano4nc  6150  ncspw1eu  6159  fce  6188