Theorem sylan 283

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  sylanb  284  sylanbr  285  syl2an  289  sylanl1  402  sylanl2  403  mpanl1  434  mpanl2  435  syldanl  449  adantll  476  adantlr  477  ancom1s  571  pm4.55dc  946  dfifp2dc  989  3adantl1  1179  3adantl2  1180  3adantl3  1181  syl3anl1  1321  syl3anl3  1323  syl3anl  1324  stoic3  1475  eupick  2159  csbiebt  3167  csbnestgf  3180  reuss2  3487  mpteq12  4172  otexg  4322  opelopabt  4356  sonr  4414  sotr  4415  issod  4416  so2nr  4418  so3nr  4419  ordelss  4476  onelon  4481  elrnmpt1s  4982  iota2  5316  funeu  5351  imadif  5410  fnbr  5434  feu  5519  f1ss  5548  f1ssres  5551  f1resf1  5552  dffo2  5563  foco  5570  foun  5602  fun11iun  5604  ffoss  5616  funbrfv  5682  fvco3  5717  fvopab6  5743  funfvbrb  5760  elpreima  5766  ffvelcdm  5780  ffvelcdmda  5782  dffo4  5795  fmptco  5813  fsn2  5821  fncofn  5832  fvconst2g  5868  fex  5883  funfvima  5886  f1elima  5914  f1ocnvfv1  5918  f1ocnvfv2  5919  cocan2  5929  foeqcnvco  5931  isocnv  5952  isores2  5954  isoini  5959  isoselem  5961  f1oiso  5967  f1ofveu  6006  eloprabga  6108  suppssof1  6253  ofco  6254  offveqb  6255  ofc1g  6257  ofc2g  6258  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  fnexALT  6273  f1dmex  6278  ot1stg  6315  ot2ndg  6316  ot3rdgg  6317  eqopi  6335  2ndrn  6346  fo2ndf  6392  smores3  6459  smores2  6460  smoel  6466  smoiso  6468  tfrlem1  6474  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemiubacc  6496  tfr1onlemsucaccv  6507  tfr1onlembfn  6510  tfr1onlemubacc  6512  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembfn  6523  tfrcllemubacc  6525  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  frecrdg  6574  omv2  6633  nnasuc  6644  nnmsuc  6645  nnacom  6652  nnaass  6653  nnmass  6655  nntri1  6664  nndifsnid  6675  nnmordi  6684  swoer  6730  erth  6748  riinerm  6777  qliftlem  6782  ecovass  6813  ecoviass  6814  elmapssres  6842  fvixp  6872  f1domg  6931  domssr  6951  endomtr  6964  xpsnen2g  7013  enen1  7026  enen2  7027  domen1  7028  domen2  7029  mapen  7032  mapxpen  7034  ssenen  7037  phplem1  7038  fidifsnid  7058  findcard  7077  findcard2  7078  findcard2s  7079  fidcen  7088  fieq0  7175  isotilem  7205  supisolem  7207  inflbti  7223  ordiso2  7234  djuex  7242  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  ctssdccl  7310  enumctlemm  7313  nnnninf  7325  finomni  7339  pm54.43  7395  acfun  7422  ccfunen  7483  cc2lem  7485  cc3  7487  addclpi  7547  addasspig  7550  mulasspig  7552  addnidpig  7556  nnppipi  7563  ltanqi  7622  ltmnqi  7623  ltexnqq  7628  archnqq  7637  prarloclemarch2  7639  enq0sym  7652  enq0tr  7654  nqnq0pi  7658  nqnq0  7661  mulcanenq0ec  7665  addclnq0  7671  nqpnq0nq  7673  distrnq0  7679  addassnq0lemcl  7681  addassnq0  7682  prubl  7706  prarloclemlt  7713  genpdf  7728  genipv  7729  genpelvl  7732  genpelvu  7733  genpml  7737  genpmu  7738  genprndl  7741  genprndu  7742  genpassl  7744  genpassu  7745  genpassg  7746  addnqprl  7749  addnqpru  7750  addlocpr  7756  nqprm  7762  nqprl  7771  nqpru  7772  mulnqprl  7788  mulnqpru  7789  mullocprlem  7790  mullocpr  7791  addcomprg  7798  mulcomprg  7800  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  ltprordil  7809  1idprl  7810  1idpru  7811  ltpopr  7815  ltsopr  7816  ltaddpr  7817  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  prplnqu  7840  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  aptiprleml  7859  aptiprlemu  7860  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemloc  7895  caucvgprlemladdrl  7898  caucvgprprlemml  7914  caucvgprprlemloc  7923  00sr  7989  map2psrprg  8025  suplocsrlempr  8027  suplocsrlem  8028  adddir  8170  axsuploc  8252  eqle  8271  le2tri3i  8288  mul4  8311  muladd11  8312  cnegexlem3  8356  addsub12  8392  2addsub  8393  addsubeq4  8394  subadd4  8423  negcon1  8431  negdi2  8437  negsubdi2  8438  neg2sub  8439  renegcl  8440  muladd  8563  subdir  8565  gt0ne0  8607  ltnegcon1  8643  lenegcon1  8646  eqord1  8663  eqord2  8664  recexre  8758  ltmul1  8772  recexap  8833  div12ap  8874  rerecapb  9023  p1le  9029  ltmul2  9036  gt0div  9050  ge0div  9051  zlem1lt  9536  nnaddm1cl  9541  zdceq  9555  gtndiv  9575  prime  9579  msqznn  9580  btwnz  9599  uzss  9777  eluzadd  9785  nn0pzuz  9821  supinfneg  9829  infsupneg  9830  divfnzn  9855  qnegcl  9870  qreccl  9876  elpqb  9884  xaddass  10104  xleadd1a  10108  xlesubadd  10118  elico2  10172  iccss  10176  iccsupr  10201  elfz5  10252  fznn  10324  difelfznle  10370  fzoaddel  10433  elincfzoext  10439  qdceq  10505  qbtwnxr  10518  flqbi2  10552  adddivflid  10553  fldivnn0  10556  divfl0  10557  flqmulnn0  10560  fldivnn0le  10564  fldiv4p1lem1div2  10566  ceiqle  10576  flqdiv  10584  modqmulnn  10605  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgdomlem  10680  frecuzrdgfunlem  10682  frecuzrdgsuctlem  10686  seqm1g  10737  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemkle  10760  seq3f1olemp  10778  seqf1oglem2  10783  seqf1og  10784  seq3id  10788  seq3z  10791  expap0  10832  mulexp  10841  mulexpzap  10842  expmul  10847  leexp1a  10857  expubnd  10859  zesq  10921  bernneq  10923  bernneq3  10925  modqexp  10929  facdiv  11001  facndiv  11002  faclbnd3  11006  faclbnd6  11007  bccmpl  11017  bcpasc  11029  bccl  11030  seq3coll  11107  fundm2domnop  11114  wrdsymb1  11154  ccatfv0  11184  ccatrn  11190  ccat2s1cl  11214  lswccats1fst  11225  swrdspsleq  11252  pfxtrcfv  11278  pfxsuffeqwrdeq  11283  pfxlswccat  11298  wrdeqs1cat  11305  cats1un  11306  swrdccatin1  11310  pfxccatin12lem4  11311  swrdccatin2  11314  pfxccatin12  11318  swrdccat  11320  shftlem  11381  ovshftex  11384  shftval4  11393  shftf  11395  shftcan2  11400  crim  11423  mulreap  11429  remul2  11438  immul2  11445  cjexp  11458  caucvgre  11546  r19.2uz  11558  sqrtsq2  11608  absnid  11638  absexp  11644  nn0abscl  11650  abslt  11653  lenegsq  11660  cau3lem  11679  minmax  11795  xrmaxadd  11826  clim  11846  climshftlemg  11867  climcn1  11873  climcn1lem  11884  clim2ser  11902  clim2ser2  11903  iserex  11904  isermulc2  11905  climub  11909  climcaucn  11916  serf0  11917  summodclem3  11946  summodclem2a  11947  summodclem2  11948  summodc  11949  fsum3  11953  fsumf1o  11956  fisumss  11958  isumss2  11959  fsumcl2lem  11964  fsumadd  11972  fsumsplit  11973  isummulc2  11992  fsum2d  12001  fsummulc2  12014  telfsumo  12032  fsumparts  12036  hash2iun1dif1  12046  bcxmas  12055  isumshft  12056  isumsplit  12057  expcnvap0  12068  geolim  12077  geolim2  12078  cvgratnnlemmn  12091  cvgratnnlemseq  12092  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  clim2divap  12106  prodmodclem3  12141  prodmodclem2a  12142  fprodseq  12149  fprodf1o  12154  fprodmul  12157  fprodsplitdc  12162  efcllemp  12224  reefcl  12234  efcj  12239  efaddlem  12240  efexp  12248  reeftlcl  12255  eftlub  12256  efsep  12257  effsumlt  12258  eflegeo  12267  retanclap  12288  demoivre  12339  demoivreALT  12340  eirraplem  12343  dvdsval3  12357  p1modz1  12360  iddvdsexp  12381  alzdvds  12420  addmodlteqALT  12425  nnehalf  12470  nno  12472  ndvdsadd  12497  bitsp1e  12518  bitsp1o  12519  bitsinv1  12528  divgcdnnr  12552  neggcd  12559  gcdabs  12564  bezoutlemmain  12574  bezoutlemaz  12579  bezoutlembz  12580  gcdmultiplez  12597  gcdzeq  12598  dvdssq  12607  nninfctlemfo  12616  algrf  12622  algcvg  12625  algcvga  12628  algfx  12629  eucalgf  12632  eucalgcvga  12635  neglcm  12652  lcmabs  12653  lcmdvds  12656  lcmgcdeq  12660  qredeq  12673  isprm3  12695  coprm  12721  prmrp  12722  isprm6  12724  prmdvdsexpb  12726  rpexp  12730  cncongrprm  12734  sqrt2irraplemnn  12756  phibndlem  12793  phiprmpw  12799  eulerthlemh  12808  eulerthlemth  12809  fermltl  12811  prmdivdiv  12814  modprm1div  12825  m1dvdsndvds  12826  coprimeprodsq  12835  pczpre  12875  pczcl  12876  pcexp  12887  pczdvds  12892  pczndvds  12894  pczndvds2  12896  pcdvdsb  12898  pcneg  12903  pcprmpw  12912  difsqpwdvds  12916  pcmptcl  12920  pcprod  12924  fldivp1  12926  infpnlem2  12938  1arithlem4  12944  ennnfonelemrn  13045  topnidg  13340  pwselbasb  13381  pwsplusgval  13383  pwsmulrval  13384  imasaddfnlemg  13402  imasaddflemg  13404  qusin  13414  mgmlrid  13467  mndass  13512  prdsidlem  13535  mhmco  13578  gsumsubm  13582  gsumwcl  13585  gsumwmhm  13586  grpass  13597  grpinvex  13598  dfgrp2  13615  grplid  13619  grprid  13620  grprcan  13625  grpinvssd  13665  grpinvval2  13671  prdsinvlem  13696  pwsinvg  13700  mhmid  13707  mhmmnd  13708  ghmgrp  13710  mulgnn  13718  mulgnnp1  13722  mulgnegnn  13724  mulgnnsubcl  13726  mulgz  13742  issubg2m  13781  issubg4m  13785  subgintm  13790  nmzbi  13801  eqger  13816  eqgid  13818  eqgen  13819  qusgrp  13824  qusadd  13826  qusinv  13828  qussub  13829  ghminv  13842  ghmsub  13843  ghmrn  13849  resghm2b  13854  ghmf1  13865  conjsubg  13869  conjsubgen  13870  qusghm  13874  cmncom  13894  ablsubadd  13904  ablsubsub23  13917  ghmcmn  13919  gsumfzreidx  13929  mgpress  13950  srg1expzeq1  14014  ringinvnz1ne0  14068  ringinvnzdiv  14069  dvdsrd  14114  dvdsunit  14132  unitinvcl  14143  unitinvinv  14144  unitlinv  14146  unitrinv  14147  rhmunitinv  14198  subrngintm  14232  subrg1  14251  subrguss  14256  subrginv  14257  subrgunit  14259  subrgugrp  14260  subrgintm  14263  resrhm  14268  resrhm2b  14269  lmodass  14323  lmodlcan  14324  lmod0vlid  14338  lmod0vrid  14339  lmod0vid  14340  lmodvs0  14342  lcomf  14347  lmodvnegcl  14348  lmodvnegid  14349  lmodvsubadd  14358  lmodsubid  14367  lss1d  14403  lspval  14410  lspsnel6  14428  lspsnneg  14440  sralmod  14470  dflidl2rng  14501  lidlacl  14504  dflidl2  14508  df2idl2  14529  qusmul2  14549  quscrng  14553  cnfldmulg  14596  znf1o  14671  znidom  14677  psraddcl  14700  psr0lid  14702  tgss3  14808  clsval  14841  clsss3  14860  neiss2  14872  resttop  14900  resttopon2  14908  lmconst  14946  cnima  14950  cnntri  14954  cncnp  14960  cnrest  14965  cndis  14971  lmss  14976  lmff  14979  lmtopcnp  14980  txcnp  15001  upxp  15002  uptx  15004  cnmpt11  15013  hmeoima  15040  hmeoopn  15041  hmeocld  15042  hmeontr  15043  hmeoimaf1o  15044  mettri2  15092  met0  15094  metres2  15111  blpnf  15130  xblss2ps  15134  xblss2  15135  blbas  15163  blres  15164  xmetec  15167  mopnss  15180  xmstri2  15200  mstri2  15201  xmstri  15202  mstri  15203  xmstri3  15204  mstri3  15205  msrtri  15206  mopni3  15214  unimopn  15216  comet  15229  bdxmet  15231  climcncf  15314  dedekindeulemuub  15347  dedekindicclemuub  15356  ivthdichlem  15381  dvfgg  15418  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvfre  15440  dvmptfsum  15455  plyadd  15481  plymul  15482  reeff1olem  15501  reeff1o  15503  sinperlem  15538  abssinper  15576  reexplog  15601  relogexp  15602  cxpexpnn  15626  cxprec  15640  rpcxpmul2  15643  abscxp  15645  wilthlem1  15710  sgmval2  15714  sgmnncl  15718  0sgmppw  15723  perfectlem1  15729  lgsdir  15770  lgsprme0  15777  lgsdinn0  15783  gausslemma2dlem3  15798  gausslemma2dlem5a  15800  2lgslem1a2  15822  2lgslem1a  15823  2lgslem3  15836  2lgs  15839  umgredgprv  15972  umgrislfupgrdom  15988  uspgredgiedg  16035  uspgriedgedg  16036  usgrislfuspgrdom  16047  usgredg2en  16052  usgredgprv  16053  usgrpredgv  16055  usgredg  16057  usgrnloopv  16058  usgredgne  16061  usgredg3  16071  usgredgedg  16084  usgredgdomord  16087  usgr1vr  16105  subgruhgrfun  16125  subupgr  16130  subumgr  16131  subusgr  16132  umgrwlknloop  16225  wlkres  16236  clwwlkccatlem  16257  clwwlkccat  16258  depindlem1  16351  depindlem2  16352  depindlem3  16353  bj-inex  16528  bj-nn0suc  16585  bj-nn0sucALT  16599  trilpolemeq1  16670  trilpolemlt1  16671  trirec0  16674  nconstwlpolemgt0  16694