Theorem syl5ibrcom 213

Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)

Hypotheses

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

Assertion

Ref	Expression
syl5ibrcom	|- (ph -> (ch -> ps))

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		syl5ibr.1	. . 3 |- (ph -> th)
2		syl5ibr.2	. . 3 |- (ch -> (ps <-> th))
3	1, 2	syl5ibr 212	. 2 |- (ch -> (ph -> ps))
4	3	com12 27	1 |- (ph -> (ch -> ps))

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:  biimprcd  216  nfsb4t  2080  elsnc2g  3761  pwadjoin  4119  opkth1g  4130  pw1disj  4167  eqpw1uni  4330  nnc0suc  4412  nndisjeq  4429  leltfintr  4458  lefinlteq  4463  lenltfin  4469  ncfinraise  4481  tfindi  4496  tfinsuc  4498  evenodddisj  4516  nnadjoin  4520  nnpweq  4523  sfinltfin  4535  vfin1cltv  4547  nulnnn  4556  funcnvuni  5161  foco2  5426  fsn  5432  fconst2g  5452  funfvima  5459  fntxp  5804  fnpprod  5843  enadjlem1  6059  enmap2lem3  6065  ncdisjun  6136  dflec2  6210  lectr  6211  leaddc1  6214  tlecg  6229  ce0tb  6237  ce0lenc1  6238  nclenn  6248  addcdi  6249  muc0or  6251  lemuc1  6252  lecadd2  6265  ncslesuc  6266  nmembers1lem3  6269  nncdiv3  6275  nnc3n3p1  6276  nchoicelem1  6287  nchoicelem2  6288  nchoicelem6  6292