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  2566  necon2d  2567  necon4ad  2578  necon4d  2580  necon1bd  2585  spcimgft  2931  eqsbc2  3104  reupick  3540  evenodddisj  4517  sfinltfin  4536  vfin1cltv  4548  dmcosseq  4974  iss  5001  xp11  5057  ssrnres  5060  opelf  5236  mapsn  6027