Theorem sylan 277

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 114	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	mpan9 275	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  sylanb  278  sylanbr  279  syl2an  283  sylanl1  394  sylanl2  395  mpanl1  424  mpanl2  425  adantll  459  adantlr  460  ancom1s  533  3adantl1  1094  3adantl2  1095  3adantl3  1096  syl3anl1  1217  syl3anl3  1219  syl3anl  1220  stoic3  1360  eupick  2020  csbiebt  2942  csbnestgf  2954  reuss2  3244  mpteq12  3861  otexg  3985  opelopabt  4017  sonr  4072  sotr  4073  issod  4074  so2nr  4076  so3nr  4077  ordelss  4134  onelon  4139  elrnmpt1s  4602  iota2  4913  funeu  4946  imadif  4999  fnbr  5021  feu  5092  f1ss  5117  f1ssres  5119  dffo2  5130  foco  5136  foun  5165  fun11iun  5167  ffoss  5178  funbrfv  5233  fvco3  5265  fvopab6  5285  funfvbrb  5301  elpreima  5307  ffvelrn  5321  ffvelrnda  5323  dffo4  5336  foelrn  5338  fmptco  5351  fsn2  5358  fvconst2g  5396  fex  5409  funfvima  5411  f1elima  5433  f1ocnvfv1  5437  f1ocnvfv2  5438  cocan2  5448  foeqcnvco  5450  isocnv  5471  isores2  5473  isoini  5477  isoselem  5479  f1oiso  5485  f1ofveu  5520  eloprabga  5611  grprinvlem  5715  suppssof1  5748  ofco  5749  offveqb  5750  fnexALT  5760  f1dmex  5763  ot1stg  5799  ot2ndg  5800  ot3rdgg  5801  eqopi  5818  2ndrn  5829  fo2ndf  5868  smores3  5931  smores2  5932  smoel  5938  smoiso  5940  tfrlem1  5946  tfrlemisucaccv  5962  tfrlemibxssdm  5964  tfrlemiubacc  5967  rdgon  5996  frecrdg  6015  freccl  6016  omv2  6068  nnasuc  6078  nnmsuc  6079  nnacom  6086  nnaass  6087  nnmass  6089  nntri1  6097  nnmordi  6112  swoer  6157  erth  6173  riinerm  6202  qliftlem  6207  ecovass  6238  ecoviass  6239  f1domg  6261  endomtr  6293  xpsnen2g  6326  enen1  6334  enen2  6335  domen1  6336  domen2  6337  phplem1  6338  findcard  6372  findcard2  6373  findcard2s  6374  isotilem  6419  supisolem  6421  inflbti  6437  ordiso2  6446  pm54.43  6459  addclpi  6517  addasspig  6520  mulasspig  6522  addnidpig  6526  nnppipi  6533  ltanqi  6592  ltmnqi  6593  ltexnqq  6598  archnqq  6607  prarloclemarch2  6609  enq0sym  6622  enq0tr  6624  nqnq0pi  6628  nqnq0  6631  mulcanenq0ec  6635  addclnq0  6641  nqpnq0nq  6643  distrnq0  6649  addassnq0lemcl  6651  addassnq0  6652  prubl  6676  prarloclemlt  6683  genpdf  6698  genipv  6699  genpelvl  6702  genpelvu  6703  genpml  6707  genpmu  6708  genprndl  6711  genprndu  6712  genpassl  6714  genpassu  6715  genpassg  6716  addnqprl  6719  addnqpru  6720  addlocpr  6726  nqprm  6732  nqprl  6741  nqpru  6742  mulnqprl  6758  mulnqpru  6759  mullocprlem  6760  mullocpr  6761  addcomprg  6768  mulcomprg  6770  distrlem1prl  6772  distrlem1pru  6773  distrlem4prl  6774  distrlem4pru  6775  ltprordil  6779  1idprl  6780  1idpru  6781  ltpopr  6785  ltsopr  6786  ltaddpr  6787  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemfl  6799  ltexprlemrl  6800  ltexprlemfu  6801  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  prplnqu  6810  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1l  6825  recexprlemss1u  6826  aptiprleml  6829  aptiprlemu  6830  cauappcvgprlemloc  6842  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemloc  6865  caucvgprlemladdrl  6868  caucvgprprlemml  6884  caucvgprprlemloc  6893  00sr  6946  adddir  7110  eqle  7202  le2tri3i  7219  mul4  7240  muladd11  7241  cnegexlem3  7285  addsub12  7321  2addsub  7322  addsubeq4  7323  subadd4  7352  negcon1  7360  negdi2  7366  negsubdi2  7367  neg2sub  7368  renegcl  7369  muladd  7488  subdir  7490  gt0ne0  7531  ltnegcon1  7567  lenegcon1  7570  recexre  7678  ltmul1  7692  recexap  7743  div12ap  7782  p1le  7927  ltmul2  7934  gt0div  7948  ge0div  7949  zlem1lt  8407  nnaddm1cl  8412  zdceq  8423  gtndiv  8442  prime  8446  msqznn  8447  btwnz  8466  uzss  8639  eluzadd  8647  nn0pzuz  8675  supinfneg  8683  infsupneg  8684  divfnzn  8706  qnegcl  8721  qreccl  8727  elico2  8960  iccss  8964  iccsupr  8989  elfz5  9037  fznn  9106  difelfznle  9146  fzoaddel  9201  qdceq  9256  qbtwnxr  9266  flqbi2  9293  adddivflid  9294  fldivnn0  9297  divfl0  9298  flqmulnn0  9301  fldivnn0le  9305  fldiv4p1lem1div2  9307  ceiqle  9315  flqdiv  9323  modqmulnn  9344  frec2uzzd  9402  frecuzrdgfn  9414  frecuzrdgcl  9415  frecuzrdgsuc  9417  iseqsplit  9458  iseqcaopr2  9461  iseqid  9467  iseqz  9469  expap0  9506  mulexp  9515  mulexpzap  9516  expmul  9521  leexp1a  9531  expubnd  9533  zesq  9591  bernneq  9593  bernneq3  9595  facdiv  9665  facndiv  9666  faclbnd3  9670  faclbnd6  9671  bccmpl  9681  bcpasc  9693  bccl  9694  shftlem  9704  ovshftex  9707  shftval4  9716  shftf  9718  shftcan2  9723  crim  9745  mulreap  9751  remul2  9760  immul2  9767  cjexp  9780  caucvgre  9867  r19.2uz  9879  sqrtsq2  9929  absnid  9959  absexp  9965  nn0abscl  9971  abslt  9974  lenegsq  9981  cau3lem  10000  minmax  10112  clim  10120  climshftlemg  10141  climcn1  10147  climcn1lem  10157  clim2iser  10175  clim2iser2  10176  iiserex  10177  iisermulc2  10178  climub  10182  climcaucn  10188  serif0  10189  dvdsval3  10199  iddvdsexp  10219  alzdvds  10254  addmodlteqALT  10259  nnehalf  10304  nno  10306  ndvdsadd  10331  divgcdnnr  10367  neggcd  10374  gcdabs  10379  bezoutlemmain  10387  bezoutlemaz  10392  bezoutlembz  10393  gcdmultiplez  10410  gcdzeq  10411  dvdssq  10420  ialgcvg  10430  ialgcvga  10433  ialgfx  10434  eucalgf  10437  eucialgcvga  10440  neglcm  10457  lcmabs  10458  lcmdvds  10461  lcmgcdeq  10465  qredeq  10478  isprm3  10500  coprm  10523  prmrp  10524  isprm6  10526  prmdvdsexpb  10528  rpexp  10532  cncongrprm  10536  sqrt2irraplemnn  10557  bj-inex  10698  bj-nn0suc  10759  bj-nn0sucALT  10773