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-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  biimprcd  216  nfsb4t  2080  elsnc2g  3762  pwadjoin  4120  opkth1g  4131  pw1disj  4168  eqpw1uni  4331  nnc0suc  4413  nndisjeq  4430  leltfintr  4459  lefinlteq  4464  lenltfin  4470  ncfinraise  4482  tfindi  4497  tfinsuc  4499  evenodddisj  4517  nnadjoin  4521  nnpweq  4524  sfinltfin  4536  vfin1cltv  4548  nulnnn  4557  funcnvuni  5162  foco2  5427  fsn  5433  fconst2g  5453  funfvima  5460  fntxp  5805  fnpprod  5844  enadjlem1  6060  enmap2lem3  6066  ncdisjun  6137  dflec2  6211  lectr  6212  leaddc1  6215  tlecg  6231  ce0tb  6239  ce0lenc1  6240  nclenn  6250  addcdi  6251  muc0or  6253  lemuc1  6254  lecadd2  6267  ncslesuc  6268  nmembers1lem3  6271  nncdiv3  6278  nnc3n3p1  6279  nchoicelem1  6290  nchoicelem2  6291  nchoicelem6  6295