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  406  sylanl2  407  mpanl1  438  mpanl2  439  syldanl  453  adantll  480  adantlr  481  ancom1s  575  pm4.55dc  951  dfifp2dc  994  3adantl1  1184  3adantl2  1185  3adantl3  1186  syl3anl1  1326  syl3anl3  1328  syl3anl  1329  stoic3  1480  eupick  2166  csbiebt  3187  csbnestgf  3200  reuss2  3513  mpteq12  4212  otexg  4368  opelopabt  4402  sonr  4460  sotr  4461  issod  4462  so2nr  4464  so3nr  4465  ordelss  4522  onelon  4527  elrnmpt1s  5030  iota2  5365  funeu  5400  imadif  5459  fnbr  5483  feu  5572  f1ss  5602  f1ssres  5605  f1resf1  5606  dffo2  5617  foco  5624  foun  5656  fun11iun  5658  ffoss  5670  funbrfv  5736  fvco3  5773  fvopab6  5799  funfvbrb  5816  elpreima  5822  ffvelcdm  5835  ffvelcdmda  5837  dffo4  5850  fmptco  5868  fsn2  5876  fncofn  5887  fvconst2g  5923  fex  5941  funfvima  5944  f1elima  5973  f1ocnvfv1  5977  f1ocnvfv2  5978  cocan2  5988  foeqcnvco  5990  isocnv  6011  isores2  6013  isoini  6018  isoselem  6020  f1oiso  6026  f1ofveu  6067  eloprabga  6169  suppssof1  6314  ofco  6315  offveqb  6316  ofc1g  6318  ofc2g  6319  caofid0l  6323  caofid0r  6324  caofid1  6325  caofid2  6326  fnexALT  6334  f1dmex  6339  ot1stg  6380  ot2ndg  6381  ot3rdgg  6382  eqopi  6400  2ndrn  6411  fo2ndf  6457  suppval1  6473  ressuppss  6488  suppssrst  6495  suppssrgst  6496  smores3  6558  smores2  6559  smoel  6565  smoiso  6567  tfrlem1  6573  tfrlemisucaccv  6590  tfrlemibxssdm  6592  tfrlemiubacc  6595  tfr1onlemsucaccv  6606  tfr1onlembfn  6609  tfr1onlemubacc  6611  tfr1onlemaccex  6613  tfr1onlemres  6614  tfrcllemsucaccv  6619  tfrcllembfn  6622  tfrcllemubacc  6624  tfrcllemaccex  6626  tfrcllemres  6627  tfrcl  6629  frecrdg  6673  omv2  6732  nnasuc  6743  nnmsuc  6744  nnacom  6751  nnaass  6752  nnmass  6754  nntri1  6763  nndifsnid  6774  nnmordi  6783  swoer  6829  erth  6847  riinerm  6876  qliftlem  6881  ecovass  6912  ecoviass  6913  elmapssres  6948  fvixp  6979  f1domg  7038  domssr  7058  endomtr  7071  xpsnen2g  7121  enen1  7134  enen2  7135  domen1  7136  domen2  7137  mapen  7140  mapxpen  7142  ssenen  7146  phplem1  7147  fidifsnid  7167  findcard  7186  findcard2  7187  findcard2s  7188  fidcen  7197  fieq0  7304  isotilem  7340  supisolem  7342  inflbti  7358  ordiso2  7369  djuex  7377  updjudhcoinlf  7414  updjudhcoinrg  7415  updjud  7416  ctssdccl  7445  enumctlemm  7448  nnnninf  7460  finomni  7474  pm54.43  7530  acfun  7557  ccfunen  7624  cc2lem  7626  cc3  7628  addclpi  7688  addasspig  7691  mulasspig  7693  addnidpig  7697  nnppipi  7704  ltanqi  7763  ltmnqi  7764  ltexnqq  7769  archnqq  7778  prarloclemarch2  7780  enq0sym  7793  enq0tr  7795  nqnq0pi  7799  nqnq0  7802  mulcanenq0ec  7806  addclnq0  7812  nqpnq0nq  7814  distrnq0  7820  addassnq0lemcl  7822  addassnq0  7823  prubl  7847  prarloclemlt  7854  genpdf  7869  genipv  7870  genpelvl  7873  genpelvu  7874  genpml  7878  genpmu  7879  genprndl  7882  genprndu  7883  genpassl  7885  genpassu  7886  genpassg  7887  addnqprl  7890  addnqpru  7891  addlocpr  7897  nqprm  7903  nqprl  7912  nqpru  7913  mulnqprl  7929  mulnqpru  7930  mullocprlem  7931  mullocpr  7932  addcomprg  7939  mulcomprg  7941  distrlem1prl  7943  distrlem1pru  7944  distrlem4prl  7945  distrlem4pru  7946  ltprordil  7950  1idprl  7951  1idpru  7952  ltpopr  7956  ltsopr  7957  ltaddpr  7958  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemlol  7963  ltexprlemopu  7964  ltexprlemupu  7965  ltexprlemdisj  7967  ltexprlemloc  7968  ltexprlemfl  7970  ltexprlemrl  7971  ltexprlemfu  7972  ltexprlemru  7973  addcanprleml  7975  addcanprlemu  7976  prplnqu  7981  recexprlemloc  7992  recexprlem1ssl  7994  recexprlem1ssu  7995  recexprlemss1l  7996  recexprlemss1u  7997  aptiprleml  8000  aptiprlemu  8001  cauappcvgprlemloc  8013  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  caucvgprlemloc  8036  caucvgprlemladdrl  8039  caucvgprprlemml  8055  caucvgprprlemloc  8064  00sr  8130  map2psrprg  8166  suplocsrlempr  8168  suplocsrlem  8169  adddir  8311  axsuploc  8392  eqle  8411  le2tri3i  8428  mul4  8452  muladd11  8453  cnegexlem3  8497  addsub12  8533  2addsub  8534  addsubeq4  8535  subadd4  8564  negcon1  8572  negdi2  8578  negsubdi2  8579  neg2sub  8580  renegcl  8581  muladd  8705  subdir  8707  gt0ne0  8749  ltnegcon1  8785  lenegcon1  8788  eqord1  8805  eqord2  8806  recexre  8900  ltmul1  8914  recexap  8975  div12ap  9018  rerecapb  9167  p1le  9173  ltmul2  9180  gt0div  9194  ge0div  9195  zlem1lt  9684  nnaddm1cl  9689  zdceq  9703  gtndiv  9724  prime  9728  msqznn  9729  btwnz  9748  uzss  9926  eluzadd  9934  nn0pzuz  9970  supinfneg  9978  infsupneg  9979  divfnzn  10004  qnegcl  10019  qreccl  10025  elpqb  10033  xaddass  10254  xleadd1a  10258  xlesubadd  10268  elico2  10322  iccss  10326  iccsupr  10351  elfz5  10403  fznn  10479  difelfznle  10525  fzoaddel  10588  elincfzoext  10594  qdceq  10662  qbtwnxr  10675  flqbi2  10709  adddivflid  10710  fldivnn0  10713  divfl0  10714  flqmulnn0  10717  fldivnn0le  10721  fldiv4p1lem1div2  10723  ceiqle  10733  flqdiv  10741  modqmulnn  10762  frecuzrdgtcl  10832  frecuzrdgsuc  10834  frecuzrdgdomlem  10837  frecuzrdgfunlem  10839  frecuzrdgsuctlem  10843  seqm1g  10894  seq3caopr2  10913  seqcaopr2g  10914  iseqf1olemkle  10917  seq3f1olemp  10935  seqf1oglem2  10940  seqf1og  10941  seq3id  10945  seq3z  10948  expap0  10989  mulexp  10998  mulexpzap  10999  expmul  11004  leexp1a  11014  expubnd  11016  zesq  11079  bernneq  11081  bernneq3  11083  modqexp  11087  facdiv  11159  facndiv  11160  faclbnd3  11164  faclbnd6  11165  bccmpl  11175  bcpasc  11187  bccl  11188  hashfibclem  11265  hashfibc  11266  seq3coll  11277  fundm2domnop  11284  wrdsymb1  11324  ccatfv0  11354  ccatrn  11360  ccat2s1cl  11384  lswccats1fst  11395  swrdspsleq  11422  pfxtrcfv  11448  pfxsuffeqwrdeq  11453  pfxlswccat  11468  wrdeqs1cat  11475  cats1un  11476  swrdccatin1  11480  pfxccatin12lem4  11481  swrdccatin2  11484  pfxccatin12  11488  swrdccat  11490  shftlem  11564  ovshftex  11567  shftval4  11576  shftf  11578  shftcan2  11583  crim  11606  mulreap  11612  remul2  11621  immul2  11628  cjexp  11641  caucvgre  11730  r19.2uz  11742  sqrtsq2  11792  absnid  11822  absexp  11828  nn0abscl  11834  abslt  11837  lenegsq  11844  cau3lem  11863  minmax  11979  xrmaxadd  12010  clim  12030  climshftlemg  12051  climcn1  12057  climcn1lem  12068  clim2ser  12086  clim2ser2  12087  iserex  12088  isermulc2  12089  climub  12093  climcaucn  12100  serf0  12101  summodclem3  12130  summodclem2a  12131  summodclem2  12132  summodc  12133  fsum3  12137  fsumf1o  12140  fisumss  12142  isumss2  12143  fsumcl2lem  12148  fsumadd  12156  fsumsplit  12157  isummulc2  12176  fsum2d  12185  fsummulc2  12198  telfsumo  12216  fsumparts  12220  hash2iun1dif1  12230  bcxmas  12239  isumshft  12240  isumsplit  12241  expcnvap0  12252  geolim  12261  geolim2  12262  cvgratnnlemmn  12275  cvgratnnlemseq  12276  mertenslemi1  12285  mertenslem2  12286  mertensabs  12287  clim2divap  12290  prodmodclem3  12325  prodmodclem2a  12326  fprodseq  12333  fprodf1o  12338  fprodmul  12341  fprodsplitdc  12346  efcllemp  12408  reefcl  12418  efcj  12423  efaddlem  12424  efexp  12432  reeftlcl  12439  eftlub  12440  efsep  12441  effsumlt  12442  eflegeo  12451  retanclap  12472  demoivre  12523  demoivreALT  12524  eirraplem  12527  dvdsval3  12541  p1modz1  12544  iddvdsexp  12565  alzdvds  12604  addmodlteqALT  12609  nnehalf  12654  nno  12656  ndvdsadd  12681  bitsp1e  12702  bitsp1o  12703  bitsinv1  12712  divgcdnnr  12736  neggcd  12743  gcdabs  12748  bezoutlemmain  12758  bezoutlemaz  12763  bezoutlembz  12764  gcdmultiplez  12781  gcdzeq  12782  dvdssq  12791  nninfctlemfo  12800  algrf  12806  algcvg  12809  algcvga  12812  algfx  12813  eucalgf  12816  eucalgcvga  12819  neglcm  12836  lcmabs  12837  lcmdvds  12840  lcmgcdeq  12844  qredeq  12857  isprm3  12879  coprm  12905  prmrp  12906  isprm6  12908  prmdvdsexpb  12910  rpexp  12914  cncongrprm  12918  sqrt2irraplemnn  12940  phibndlem  12977  phiprmpw  12983  eulerthlemh  12992  eulerthlemth  12993  fermltl  12995  prmdivdiv  12998  modprm1div  13009  m1dvdsndvds  13010  coprimeprodsq  13019  pczpre  13059  pczcl  13060  pcexp  13071  pczdvds  13076  pczndvds  13078  pczndvds2  13080  pcdvdsb  13082  pcneg  13087  pcprmpw  13096  difsqpwdvds  13100  pcmptcl  13104  pcprod  13108  fldivp1  13110  infpnlem2  13122  1arithlem4  13128  ballotfilem2  13211  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemfrcn0  13256  ennnfonelemrn  13293  topnidg  13589  imasaddfnlemg  13618  imasaddflemg  13620  qusin  13630  mgmlrid  13682  mndass  13720  mhmco  13780  gzsumwcl  13785  gzsumwmhm  13786  grpass  13797  grpinvex  13798  dfgrp2  13815  grplid  13819  grprid  13820  grprcan  13825  grpinvssd  13865  grpinvval2  13871  mhmid  13901  mhmmnd  13902  ghmgrp  13904  mulgnn  13912  mulgnnp1  13916  mulgnegnn  13918  mulgnnsubcl  13920  mulgz  13936  issubg2m  13975  issubg4m  13979  subgintm  13984  nmzbi  13995  eqger  14010  eqgid  14012  eqgen  14013  qusgrp  14018  qusadd  14020  qusinv  14022  qussub  14023  ghminv  14036  ghmsub  14037  ghmrn  14043  resghm2b  14048  ghmf1  14059  conjsubg  14063  conjsubgen  14064  qusghm  14068  cmncom  14088  ablsubadd  14099  ablsubsub23  14112  ghmcmn  14114  gzsumreidx  14124  gsumsubmfi  14151  prdsidlem  14176  prdsinvlem  14179  pwselbasb  14189  pwsplusgval  14191  pwsmulrval  14192  pwsinvg  14198  mgpress  14213  srg1expzeq1  14282  ringinvnz1ne0  14337  ringinvnzdiv  14338  dvdsrd  14384  dvdsunit  14402  unitinvcl  14413  unitinvinv  14414  unitlinv  14416  unitrinv  14417  rhmunitinv  14468  subrngintm  14503  subrg1  14522  subrguss  14527  subrginv  14528  subrgunit  14530  subrgugrp  14531  subrgintm  14534  resrhm  14539  resrhm2b  14540  lmodass  14622  lmodlcan  14623  lmod0vlid  14638  lmod0vrid  14639  lmod0vid  14640  lmodvs0  14642  lcomf  14647  lmodvnegcl  14648  lmodvnegid  14649  lmodvsubadd  14658  lmodsubid  14667  lss1d  14703  lspval  14710  ellspsn6  14728  lspsnneg  14740  sralmod  14770  dflidl2rng  14801  lidlacl  14804  dflidl2  14808  df2idl2  14829  qusmul2  14849  quscrng  14853  cnfldmulg  14896  znf1o  14969  znidom  14975  aspval  14998  asclghm  15008  issubassa2  15018  psraddcl  15054  psr0lid  15056  tgss3  15162  clsval  15195  clsss3  15214  neiss2  15226  resttop  15254  resttopon2  15262  lmconst  15300  cnima  15304  cnntri  15308  cncnp  15314  cnrest  15319  cndis  15325  lmss  15330  lmff  15333  lmtopcnp  15334  txcnp  15355  upxp  15356  uptx  15358  cnmpt11  15367  hmeoima  15394  hmeoopn  15395  hmeocld  15396  hmeontr  15397  hmeoimaf1o  15398  mettri2  15446  met0  15448  metres2  15465  blpnf  15484  xblss2ps  15488  xblss2  15489  blbas  15517  blres  15518  xmetec  15521  mopnss  15534  xmstri2  15554  mstri2  15555  xmstri  15556  mstri  15557  xmstri3  15558  mstri3  15559  msrtri  15560  mopni3  15568  unimopn  15570  comet  15583  bdxmet  15585  climcncf  15668  dedekindeulemuub  15701  dedekindicclemuub  15710  ivthdichlem  15735  dvfgg  15772  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvfre  15794  dvmptfsum  15809  plyadd  15835  plymul  15836  reeff1olem  15855  reeff1o  15857  sinperlem  15892  abssinper  15930  reexplog  15955  relogexp  15956  cxpexpnn  15981  cxprec  15995  rpcxpmul2  15998  abscxp  16000  wilthlem1  16077  sgmval2  16081  sgmnncl  16085  0sgmppw  16090  perfectlem1  16096  lgsdir  16137  lgsprme0  16144  lgsdinn0  16150  gausslemma2dlem3  16165  gausslemma2dlem5a  16167  2lgslem1a2  16189  2lgslem1a  16190  2lgslem3  16203  2lgs  16206  umgredgprv  16339  umgrislfupgrdom  16355  uspgredgiedg  16402  uspgriedgedg  16403  usgrislfuspgrdom  16414  usgredg2en  16419  usgredgprv  16420  usgrpredgv  16422  usgredg  16424  usgrnloopv  16425  usgredgne  16428  usgredg3  16438  usgredgedg  16451  usgredgdomord  16454  usgr1vr  16472  subgruhgrfun  16492  subupgr  16497  subumgr  16498  subusgr  16499  umgrwlknloop  16592  wlkres  16603  clwwlkccatlem  16624  clwwlkccat  16625  depindlem1  16730  depindlem2  16731  depindlem3  16732  bj-inex  16916  bj-nn0suc  16973  bj-nn0sucALT  16987  trilpolemeq1  17063  trilpolemlt1  17064  trirec0  17067  nconstwlpolemgt0  17088