Theorem sylbid 206

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem sylbid

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpd 198	. 2 |- (ph -> (ps -> ch))
3		sylbid.2	. 2 |- (ph -> (ch -> th))
4	2, 3	syld 40	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:  3imtr4d  259  ax11eq  2193  ax11el  2194  leltfintr  4459  tfin11  4494  sfinltfin  4536  phi11lem1  4596  xp11  5057  xpcan  5058  xpcan2  5059  enprmaplem3  6079  enprmaplem6  6082  ce0addcnnul  6180  ceclb  6184  fce  6189  sbth  6207  dflec2  6211  lectr  6212  leaddc1  6215  leconnnc  6219  tlecg  6231  letc  6232  ce0lenc1  6240  nclenn  6250  lemuc1  6254  lecadd2  6267  ncslesuc  6268  nchoicelem9  6298  nchoicelem12  6301  nchoicelem17  6306  dmfrec  6317  fnfreclem2  6319  fnfreclem3  6320