Theorem syl6ib 217

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

Hypotheses

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

Assertion

Ref	Expression
syl6ib	|- (ph -> (ps -> th))

Proof of Theorem syl6ib

Step	Hyp	Ref	Expression
1		syl6ib.1	. 2 |- (ph -> (ps -> ch))
2		syl6ib.2	. . 3 |- (ch <-> th)
3	2	biimpi 186	. 2 |- (ch -> th)
4	1, 3	syl6 29	1 |- (ph -> (ps -> 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  exp4a  589  mtord  641  19.23hOLD  1820  ax12olem6  1932  cbvexd  2009  ax15  2021  2eu3  2286  exists2  2294  necon2bd  2565  necon2d  2566  necon4ad  2577  necon4d  2579  necon1bd  2584  spcimgft  2930  eqsbc3r  3103  reupick  3539  evenodddisj  4516  sfinltfin  4535  vfin1cltv  4547  dmcosseq  4973  iss  5000  xp11  5056  ssrnres  5059  opelf  5235  mapsn  6026