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  6414  enq0tr  6416  nqnq0pi  6420  nqnq0  6423  mulcanenq0ec  6427  addclnq0  6433  nqpnq0nq  6435  distrnq0  6441  addassnq0lemcl  6443  addassnq0  6444  prubl  6468  prarloclemlt  6475  genpdf  6490  genipv  6491  genpelvl  6494  genpelvu  6495  genpml  6500  genpmu  6501  genprndl  6504  genprndu  6505  genpassl  6507  genpassu  6508  genpassg  6509  addnqprl  6512  addnqpru  6513  addlocpr  6519  nqprm  6525  mulnqprl  6547  mulnqpru  6548  mullocprlem  6549  mullocpr  6550  addcomprg  6552  mulcomprg  6554  distrlem1prl  6556  distrlem1pru  6557  distrlem4prl  6558  distrlem4pru  6559  ltprordil  6563  1idprl  6564  1idpru  6565  ltpopr  6567  ltsopr  6568  ltaddpr  6569  ltexprlemm  6572  ltexprlemopl  6573  ltexprlemlol  6574  ltexprlemopu  6575  ltexprlemupu  6576  ltexprlemdisj  6578  ltexprlemloc  6579  ltexprlemfl  6581  ltexprlemrl  6582  ltexprlemfu  6583  ltexprlemru  6584  addcanprleml  6586  addcanprlemu  6587  recexprlemloc  6601  recexprlem1ssl  6603  recexprlem1ssu  6604  recexprlemss1l  6605  recexprlemss1u  6606  aptiprleml  6609  aptiprlemu  6610  00sr  6657  adddir  6776  eqle  6866  le2tri3i  6883  mul4  6902  muladd11  6903  cnegexlem3  6945  addsub12  6981  2addsub  6982  addsubeq4  6983  subadd4  7011  negcon1  7019  negdi2  7025  negsubdi2  7026  neg2sub  7027  renegcl  7028  muladd  7137  subdir  7139  gt0ne0  7177  ltnegcon1  7213  lenegcon1  7216  recexre  7322  ltmul1  7336  recexap  7376  div12ap  7415  p1le  7556  ltmul2  7563  gt0div  7577  ge0div  7578  zlem1lt  8036  nnaddm1cl  8041  zdceq  8052  gtndiv  8071  prime  8073  msqznn  8074  btwnz  8093  uzss  8229  eluzadd  8237  nn0pzuz  8266  divfnzn  8292  qnegcl  8307  qreccl  8311  elico2  8536  iccss  8540  iccsupr  8565  elfz5  8612  fznn  8681  difelfznle  8723  fzoaddel  8778  frec2uzzd  8827  frecuzrdgfn  8839  frecuzrdgcl  8840  frecuzrdgsuc  8842  expap0  8899  mulexp  8908  mulexpzap  8909  expmul  8914  leexp1a  8923  expubnd  8925  zesq  8980  bernneq  8982  bernneq3  8984  crim  9046  mulreap  9052  remul2  9061  immul2  9068  cjexp  9081  bj-inex  9292  bj-nn0suc  9348  bj-nn0sucALT  9362