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  3831  otexg  3958  opelopabt  3990  sonr  4045  sotr  4046  issod  4047  so2nr  4049  so3nr  4050  ordelss  4082  onelon  4087  elrnmpt1s  4527  iota2  4836  funeu  4869  imadif  4922  fnbr  4944  feu  5015  f1ss  5040  f1ssres  5042  dffo2  5053  foco  5059  foun  5088  fun11iun  5090  ffoss  5101  funbrfv  5155  fvco3  5187  fvopab6  5207  funfvbrb  5223  elpreima  5229  ffvelrn  5243  ffvelrnda  5245  dffo4  5258  foelrn  5260  fmptco  5273  fsn2  5280  fvconst2g  5318  fex  5331  funfvima  5333  f1elima  5355  f1ocnvfv1  5360  f1ocnvfv2  5361  cocan2  5371  foeqcnvco  5373  isocnv  5394  isores2  5396  isoini  5400  isoselem  5402  f1oiso  5408  f1ofveu  5443  eloprabga  5533  grprinvlem  5637  suppssof1  5670  ofco  5671  offveqb  5672  fnexALT  5682  f1dmex  5685  ot1stg  5721  ot2ndg  5722  ot3rdgg  5723  eqopi  5740  2ndrn  5751  fo2ndf  5790  smores3  5849  smores2  5850  smoel  5856  smoiso  5858  tfrlem1  5864  tfrlemisucaccv  5880  tfrlemibxssdm  5882  tfrlemiubacc  5885  rdgon  5913  frecrdg  5931  freccl  5932  omv2  5984  nnasuc  5994  nnmsuc  5995  nnacom  6002  nnaass  6003  nnmass  6005  nntri1  6013  nnmordi  6025  swoer  6070  erth  6086  riinerm  6115  qliftlem  6120  ecovass  6151  ecoviass  6152  f1domg  6174  endomtr  6206  xpsnen2g  6239  enen1  6247  enen2  6248  domen1  6249  domen2  6250  addclpi  6311  addasspig  6314  mulasspig  6316  addnidpig  6320  nnppipi  6327  ltanqi  6386  ltmnqi  6387  ltexnqq  6391  archnqq  6400  prarloclemarch2  6402  enq0sym  6415  enq0tr  6417  nqnq0pi  6421  nqnq0  6424  mulcanenq0ec  6428  addclnq0  6434  nqpnq0nq  6436  distrnq0  6442  addassnq0lemcl  6444  addassnq0  6445  prubl  6469  prarloclemlt  6476  genpdf  6491  genipv  6492  genpelvl  6495  genpelvu  6496  genpml  6500  genpmu  6501  genprndl  6504  genprndu  6505  genpassl  6507  genpassu  6508  genpassg  6509  addnqprl  6512  addnqpru  6513  addlocpr  6519  nqprm  6525  nqprl  6533  mulnqprl  6549  mulnqpru  6550  mullocprlem  6551  mullocpr  6552  addcomprg  6554  mulcomprg  6556  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  ltprordil  6565  1idprl  6566  1idpru  6567  ltpopr  6569  ltsopr  6570  ltaddpr  6571  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemlol  6576  ltexprlemopu  6577  ltexprlemupu  6578  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  recexprlemss1u  6608  aptiprleml  6611  aptiprlemu  6612  cauappcvgprlemloc  6624  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemloc  6646  caucvgprlemladdrl  6649  00sr  6697  adddir  6816  eqle  6906  le2tri3i  6923  mul4  6942  muladd11  6943  cnegexlem3  6985  addsub12  7021  2addsub  7022  addsubeq4  7023  subadd4  7051  negcon1  7059  negdi2  7065  negsubdi2  7066  neg2sub  7067  renegcl  7068  muladd  7177  subdir  7179  gt0ne0  7217  ltnegcon1  7253  lenegcon1  7256  recexre  7362  ltmul1  7376  recexap  7416  div12ap  7455  p1le  7596  ltmul2  7603  gt0div  7617  ge0div  7618  zlem1lt  8076  nnaddm1cl  8081  zdceq  8092  gtndiv  8111  prime  8113  msqznn  8114  btwnz  8133  uzss  8269  eluzadd  8277  nn0pzuz  8306  divfnzn  8332  qnegcl  8347  qreccl  8351  elico2  8576  iccss  8580  iccsupr  8605  elfz5  8652  fznn  8721  difelfznle  8763  fzoaddel  8818  frec2uzzd  8867  frecuzrdgfn  8879  frecuzrdgcl  8880  frecuzrdgsuc  8882  expap0  8939  mulexp  8948  mulexpzap  8949  expmul  8954  leexp1a  8963  expubnd  8965  zesq  9020  bernneq  9022  bernneq3  9024  crim  9086  mulreap  9092  remul2  9101  immul2  9108  cjexp  9121  absnid  9227  nn0abscl  9229  bj-inex  9362  bj-nn0suc  9424  bj-nn0sucALT  9438