Theorem sylan 267

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 109	. 2 ⊢ (χ → (ψ → θ))
4	1, 3	mpan9 265	1 ⊢ ((φ ∧ χ) → θ)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  sylanb  268  sylanbr  269  syl2an  273  sylanl1  382  sylanl2  383  mpanl1  410  mpanl2  411  adantll  445  adantlr  446  ancom1s  503  3adantl1  1059  3adantl2  1060  3adantl3  1061  syl3anl1  1182  syl3anl3  1184  syl3anl  1185  stoic3  1317  eupick  1976  csbiebt  2880  csbnestgf  2892  reuss2  3211  mpteq12  3830  otexg  3957  opelopabt  3989  sonr  4044  sotr  4045  issod  4046  so2nr  4048  so3nr  4049  ordelss  4081  onelon  4086  elrnmpt1s  4526  iota2  4835  funeu  4867  imadif  4920  fnbr  4942  feu  5013  f1ss  5038  f1ssres  5040  dffo2  5051  foco  5057  foun  5086  fun11iun  5088  ffoss  5099  funbrfv  5153  fvco3  5185  fvopab6  5205  funfvbrb  5221  elpreima  5227  ffvelrn  5241  ffvelrnda  5243  dffo4  5256  foelrn  5258  fmptco  5271  fsn2  5278  fvconst2g  5316  fex  5329  funfvima  5331  f1elima  5353  f1ocnvfv1  5358  f1ocnvfv2  5359  cocan2  5369  foeqcnvco  5371  isocnv  5392  isores2  5394  isoini  5398  isoselem  5400  f1oiso  5406  f1ofveu  5440  eloprabga  5530  grprinvlem  5634  suppssof1  5667  ofco  5668  offveqb  5669  fnexALT  5679  f1dmex  5682  ot1stg  5718  ot2ndg  5719  ot3rdgg  5720  eqopi  5737  2ndrn  5748  fo2ndf  5787  smores3  5846  smores2  5847  smoel  5853  smoiso  5855  tfrlem1  5861  tfrlemisucaccv  5877  tfrlemibxssdm  5879  tfrlemiubacc  5882  rdgon  5910  frecrdg  5925  omv2  5977  nnasuc  5987  nnmsuc  5988  nnacom  5995  nnaass  5996  nnmass  5998  nntri1  6006  nnmordi  6018  swoer  6063  erth  6079  riinerm  6108  qliftlem  6113  ecovass  6144  ecoviass  6145  f1domg  6167  endomtr  6199  xpsnen2g  6232  enen1  6240  enen2  6241  domen1  6242  domen2  6243  addclpi  6304  addasspig  6307  mulasspig  6309  addnidpig  6313  nnppipi  6320  ltanqi  6379  ltmnqi  6380  ltexnqq  6384  archnqq  6393  prarloclemarch2  6395  enq0sym  6407  enq0tr  6409  nqnq0pi  6413  nqnq0  6416  mulcanenq0ec  6420  addclnq0  6426  nqpnq0nq  6428  distrnq0  6434  addassnq0lemcl  6436  addassnq0  6437  prubl  6461  prarloclemlt  6468  genpdf  6483  genipv  6484  genpelvl  6487  genpelvu  6488  genpml  6493  genpmu  6494  genprndl  6497  genprndu  6498  genpassl  6500  genpassu  6501  genpassg  6502  addnqprl  6505  addnqpru  6506  addlocpr  6512  nqprm  6518  mulnqprl  6539  mulnqpru  6540  mullocprlem  6541  mullocpr  6542  addcomprg  6544  mulcomprg  6546  distrlem1prl  6548  distrlem1pru  6549  distrlem4prl  6550  distrlem4pru  6551  ltprordil  6555  1idprl  6556  1idpru  6557  ltpopr  6559  ltsopr  6560  ltaddpr  6561  ltexprlemm  6564  ltexprlemopl  6565  ltexprlemlol  6566  ltexprlemopu  6567  ltexprlemupu  6568  ltexprlemdisj  6570  ltexprlemloc  6571  ltexprlemfl  6573  ltexprlemrl  6574  ltexprlemfu  6575  ltexprlemru  6576  addcanprleml  6578  addcanprlemu  6579  recexprlemloc  6593  recexprlem1ssl  6595  recexprlem1ssu  6596  recexprlemss1l  6597  recexprlemss1u  6598  aptiprleml  6601  aptiprlemu  6602  00sr  6649  adddir  6768  eqle  6858  le2tri3i  6875  mul4  6894  muladd11  6895  cnegexlem3  6937  addsub12  6973  2addsub  6974  addsubeq4  6975  subadd4  7003  negcon1  7011  negdi2  7017  negsubdi2  7018  neg2sub  7019  renegcl  7020  muladd  7129  subdir  7131  gt0ne0  7169  ltnegcon1  7205  lenegcon1  7208  recexre  7314  ltmul1  7328  recexap  7368  div12ap  7407  p1le  7547  ltmul2  7554  gt0div  7568  ge0div  7569  zlem1lt  8026  nnaddm1cl  8031  zdceq  8042  gtndiv  8060  prime  8062  msqznn  8063  btwnz  8082  uzss  8218  eluzadd  8226  nn0pzuz  8255  divfnzn  8281  qnegcl  8296  qreccl  8300  elico2  8524  iccss  8528  iccsupr  8553  elfz5  8600  fznn  8667  difelfznle  8709  fzoaddel  8764  frec2uzzd  8813  bj-inex  8957  bj-nn0suc  9013  bj-nn0sucALT  9027