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-mp 5  ax-1 6  ax-2 7  ax-3 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  2579  ceqex  2970  ssdisj  3601  pssdifn0  3612  ltfintr  4460  evenodddisj  4517  sfinltfin  4536  fun11iun  5306  funopfv  5358  dff3  5421  funfvima  5460  trrd  5926  peano4nc  6151  ncspw1eu  6160  fce  6189