Theorem sylan 457

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
sylan.1	⊢ (φ → ψ)
sylan.2	⊢ ((ψ ∧ χ) → θ)

Assertion

Ref	Expression
sylan	⊢ ((φ ∧ χ) → θ)

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.1	. 2 ⊢ (φ → ψ)
2		sylan.2	. . 3 ⊢ ((ψ ∧ χ) → θ)
3	2	expcom 424	. 2 ⊢ (χ → (ψ → θ))
4	1, 3	mpan9 455	1 ⊢ ((φ ∧ χ) → θ)

Syntax hints:   → wi 4   ∧ wa 358

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  df-an 360

This theorem is referenced by:  sylanb  458  sylanbr  459  syl2an  463  sylanl1  631  sylanl2  632  mpanl1  661  mpanl2  662  adantll  694  adantlr  695  ancom1s  780  3adantl1  1111  3adantl2  1112  3adantl3  1113  syl3anl1  1230  syl3anl3  1232  syl3anl  1233  sbcom  2089  eupick  2267  sbcrext  3119  csbiebt  3172  csbnestgf  3184  reuss2  3535  opkthg  4131  iota2  4367  addcexg  4393  lefinlteq  4463  ltlefin  4468  tfinsuc  4498  eventfin  4517  oddtfin  4518  opelopabt  4699  imaexg  4746  ideqg2  4869  imadif  5171  fnbr  5185  feu  5242  fcnvres  5243  f1ss  5262  dffo2  5273  foco  5279  fun11iun  5305  ffoss  5314  fvco3  5384  fvopabg  5391  elpreima  5407  ffvelrn  5415  dffo4  5423  foelrn  5425  fsn2  5434  fvconst2g  5451  funfvima  5459  f1elima  5474  f1ocnvfv1  5476  f1ocnvfv2  5477  f1ofveu  5480  f1ocnvdm  5481  isocnv  5491  isores2  5493  isotr  5495  isoini  5497  f1oiso  5499  f1oiso2  5500  eloprabga  5578  mpteq12  5657  enprmaplem3  6078  ovmuc  6130  mucnc  6131  cenc  6181  leaddc1  6214  addccan2nc  6265  lecadd2  6266  nnc3n3p2  6279  nchoicelem4  6292  nchoicelem5  6293  nchoicelem8  6296