Theorem syl5ibrcom 213

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

Hypotheses

Ref	Expression
syl5ibr.1	⊢ (φ → θ)
syl5ibr.2	⊢ (χ → (ψ ↔ θ))

Assertion

Ref	Expression
syl5ibrcom	⊢ (φ → (χ → ψ))

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		syl5ibr.1	. . 3 ⊢ (φ → θ)
2		syl5ibr.2	. . 3 ⊢ (χ → (ψ ↔ θ))
3	1, 2	syl5ibr 212	. 2 ⊢ (χ → (φ → ψ))
4	3	com12 27	1 ⊢ (φ → (χ → ψ))

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  6230  ce0tb  6238  ce0lenc1  6239  nclenn  6249  addcdi  6250  muc0or  6252  lemuc1  6253  lecadd2  6266  ncslesuc  6267  nmembers1lem3  6270  nncdiv3  6277  nnc3n3p1  6278  nchoicelem1  6289  nchoicelem2  6290  nchoicelem6  6294