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  569  pm4.55dc  940  3adantl1  1155  3adantl2  1156  3adantl3  1157  syl3anl1  1297  syl3anl3  1299  syl3anl  1300  stoic3  1442  eupick  2124  csbiebt  3124  csbnestgf  3137  reuss2  3444  mpteq12  4117  otexg  4264  opelopabt  4297  sonr  4353  sotr  4354  issod  4355  so2nr  4357  so3nr  4358  ordelss  4415  onelon  4420  elrnmpt1s  4917  iota2  5249  funeu  5284  imadif  5339  fnbr  5363  feu  5443  f1ss  5472  f1ssres  5475  f1resf1  5476  dffo2  5487  foco  5494  foun  5526  fun11iun  5528  ffoss  5539  funbrfv  5602  fvco3  5635  fvopab6  5661  funfvbrb  5678  elpreima  5684  ffvelcdm  5698  ffvelcdmda  5700  dffo4  5713  fmptco  5731  fsn2  5739  fvconst2g  5779  fex  5794  funfvima  5797  f1elima  5823  f1ocnvfv1  5827  f1ocnvfv2  5828  cocan2  5838  foeqcnvco  5840  isocnv  5861  isores2  5863  isoini  5868  isoselem  5870  f1oiso  5876  f1ofveu  5913  eloprabga  6013  suppssof1  6157  ofco  6158  offveqb  6159  ofc1g  6161  ofc2g  6162  caofid0l  6166  caofid0r  6167  caofid1  6168  caofid2  6169  fnexALT  6177  f1dmex  6182  ot1stg  6219  ot2ndg  6220  ot3rdgg  6221  eqopi  6239  2ndrn  6250  fo2ndf  6294  smores3  6360  smores2  6361  smoel  6367  smoiso  6369  tfrlem1  6375  tfrlemisucaccv  6392  tfrlemibxssdm  6394  tfrlemiubacc  6397  tfr1onlemsucaccv  6408  tfr1onlembfn  6411  tfr1onlemubacc  6413  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucaccv  6421  tfrcllembfn  6424  tfrcllemubacc  6426  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  frecrdg  6475  omv2  6532  nnasuc  6543  nnmsuc  6544  nnacom  6551  nnaass  6552  nnmass  6554  nntri1  6563  nndifsnid  6574  nnmordi  6583  swoer  6629  erth  6647  riinerm  6676  qliftlem  6681  ecovass  6712  ecoviass  6713  elmapssres  6741  fvixp  6771  f1domg  6826  endomtr  6858  xpsnen2g  6897  enen1  6910  enen2  6911  domen1  6912  domen2  6913  mapen  6916  mapxpen  6918  ssenen  6921  phplem1  6922  fidifsnid  6941  findcard  6958  findcard2  6959  findcard2s  6960  fieq0  7051  isotilem  7081  supisolem  7083  inflbti  7099  ordiso2  7110  djuex  7118  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  ctssdccl  7186  enumctlemm  7189  nnnninf  7201  finomni  7215  pm54.43  7271  acfun  7292  ccfunen  7349  cc2lem  7351  cc3  7353  addclpi  7413  addasspig  7416  mulasspig  7418  addnidpig  7422  nnppipi  7429  ltanqi  7488  ltmnqi  7489  ltexnqq  7494  archnqq  7503  prarloclemarch2  7505  enq0sym  7518  enq0tr  7520  nqnq0pi  7524  nqnq0  7527  mulcanenq0ec  7531  addclnq0  7537  nqpnq0nq  7539  distrnq0  7545  addassnq0lemcl  7547  addassnq0  7548  prubl  7572  prarloclemlt  7579  genpdf  7594  genipv  7595  genpelvl  7598  genpelvu  7599  genpml  7603  genpmu  7604  genprndl  7607  genprndu  7608  genpassl  7610  genpassu  7611  genpassg  7612  addnqprl  7615  addnqpru  7616  addlocpr  7622  nqprm  7628  nqprl  7637  nqpru  7638  mulnqprl  7654  mulnqpru  7655  mullocprlem  7656  mullocpr  7657  addcomprg  7664  mulcomprg  7666  distrlem1prl  7668  distrlem1pru  7669  distrlem4prl  7670  distrlem4pru  7671  ltprordil  7675  1idprl  7676  1idpru  7677  ltpopr  7681  ltsopr  7682  ltaddpr  7683  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  prplnqu  7706  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  recexprlemss1u  7722  aptiprleml  7725  aptiprlemu  7726  cauappcvgprlemloc  7738  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemloc  7761  caucvgprlemladdrl  7764  caucvgprprlemml  7780  caucvgprprlemloc  7789  00sr  7855  map2psrprg  7891  suplocsrlempr  7893  suplocsrlem  7894  adddir  8036  axsuploc  8118  eqle  8137  le2tri3i  8154  mul4  8177  muladd11  8178  cnegexlem3  8222  addsub12  8258  2addsub  8259  addsubeq4  8260  subadd4  8289  negcon1  8297  negdi2  8303  negsubdi2  8304  neg2sub  8305  renegcl  8306  muladd  8429  subdir  8431  gt0ne0  8473  ltnegcon1  8509  lenegcon1  8512  eqord1  8529  eqord2  8530  recexre  8624  ltmul1  8638  recexap  8699  div12ap  8740  rerecapb  8889  p1le  8895  ltmul2  8902  gt0div  8916  ge0div  8917  zlem1lt  9401  nnaddm1cl  9406  zdceq  9420  gtndiv  9440  prime  9444  msqznn  9445  btwnz  9464  uzss  9641  eluzadd  9649  nn0pzuz  9680  supinfneg  9688  infsupneg  9689  divfnzn  9714  qnegcl  9729  qreccl  9735  elpqb  9743  xaddass  9963  xleadd1a  9967  xlesubadd  9977  elico2  10031  iccss  10035  iccsupr  10060  elfz5  10111  fznn  10183  difelfznle  10229  fzoaddel  10287  qdceq  10353  qbtwnxr  10366  flqbi2  10400  adddivflid  10401  fldivnn0  10404  divfl0  10405  flqmulnn0  10408  fldivnn0le  10412  fldiv4p1lem1div2  10414  ceiqle  10424  flqdiv  10432  modqmulnn  10453  frecuzrdgtcl  10523  frecuzrdgsuc  10525  frecuzrdgdomlem  10528  frecuzrdgfunlem  10530  frecuzrdgsuctlem  10534  seqm1g  10585  seq3caopr2  10604  seqcaopr2g  10605  iseqf1olemkle  10608  seq3f1olemp  10626  seqf1oglem2  10631  seqf1og  10632  seq3id  10636  seq3z  10639  expap0  10680  mulexp  10689  mulexpzap  10690  expmul  10695  leexp1a  10705  expubnd  10707  zesq  10769  bernneq  10771  bernneq3  10773  modqexp  10777  facdiv  10849  facndiv  10850  faclbnd3  10854  faclbnd6  10855  bccmpl  10865  bcpasc  10877  bccl  10878  seq3coll  10953  wrdsymb1  10990  shftlem  11000  ovshftex  11003  shftval4  11012  shftf  11014  shftcan2  11019  crim  11042  mulreap  11048  remul2  11057  immul2  11064  cjexp  11077  caucvgre  11165  r19.2uz  11177  sqrtsq2  11227  absnid  11257  absexp  11263  nn0abscl  11269  abslt  11272  lenegsq  11279  cau3lem  11298  minmax  11414  xrmaxadd  11445  clim  11465  climshftlemg  11486  climcn1  11492  climcn1lem  11503  clim2ser  11521  clim2ser2  11522  iserex  11523  isermulc2  11524  climub  11528  climcaucn  11535  serf0  11536  summodclem3  11564  summodclem2a  11565  summodclem2  11566  summodc  11567  fsum3  11571  fsumf1o  11574  fisumss  11576  isumss2  11577  fsumcl2lem  11582  fsumadd  11590  fsumsplit  11591  isummulc2  11610  fsum2d  11619  fsummulc2  11632  telfsumo  11650  fsumparts  11654  hash2iun1dif1  11664  bcxmas  11673  isumshft  11674  isumsplit  11675  expcnvap0  11686  geolim  11695  geolim2  11696  cvgratnnlemmn  11709  cvgratnnlemseq  11710  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  clim2divap  11724  prodmodclem3  11759  prodmodclem2a  11760  fprodseq  11767  fprodf1o  11772  fprodmul  11775  fprodsplitdc  11780  efcllemp  11842  reefcl  11852  efcj  11857  efaddlem  11858  efexp  11866  reeftlcl  11873  eftlub  11874  efsep  11875  effsumlt  11876  eflegeo  11885  retanclap  11906  demoivre  11957  demoivreALT  11958  eirraplem  11961  dvdsval3  11975  p1modz1  11978  iddvdsexp  11999  alzdvds  12038  addmodlteqALT  12043  nnehalf  12088  nno  12090  ndvdsadd  12115  bitsp1e  12136  bitsp1o  12137  bitsinv1  12146  divgcdnnr  12170  neggcd  12177  gcdabs  12182  bezoutlemmain  12192  bezoutlemaz  12197  bezoutlembz  12198  gcdmultiplez  12215  gcdzeq  12216  dvdssq  12225  nninfctlemfo  12234  algrf  12240  algcvg  12243  algcvga  12246  algfx  12247  eucalgf  12250  eucalgcvga  12253  neglcm  12270  lcmabs  12271  lcmdvds  12274  lcmgcdeq  12278  qredeq  12291  isprm3  12313  coprm  12339  prmrp  12340  isprm6  12342  prmdvdsexpb  12344  rpexp  12348  cncongrprm  12352  sqrt2irraplemnn  12374  phibndlem  12411  phiprmpw  12417  eulerthlemh  12426  eulerthlemth  12427  fermltl  12429  prmdivdiv  12432  modprm1div  12443  m1dvdsndvds  12444  coprimeprodsq  12453  pczpre  12493  pczcl  12494  pcexp  12505  pczdvds  12510  pczndvds  12512  pczndvds2  12514  pcdvdsb  12516  pcneg  12521  pcprmpw  12530  difsqpwdvds  12534  pcmptcl  12538  pcprod  12542  fldivp1  12544  infpnlem2  12556  1arithlem4  12562  ennnfonelemrn  12663  topnidg  12956  pwselbasb  12997  pwsplusgval  12999  pwsmulrval  13000  imasaddfnlemg  13018  imasaddflemg  13020  qusin  13030  mgmlrid  13083  mndass  13128  prdsidlem  13151  mhmco  13194  gsumsubm  13198  gsumwcl  13201  gsumwmhm  13202  grpass  13213  grpinvex  13214  dfgrp2  13231  grplid  13235  grprid  13236  grprcan  13241  grpinvssd  13281  grpinvval2  13287  prdsinvlem  13312  pwsinvg  13316  mhmid  13323  mhmmnd  13324  ghmgrp  13326  mulgnn  13334  mulgnnp1  13338  mulgnegnn  13340  mulgnnsubcl  13342  mulgz  13358  issubg2m  13397  issubg4m  13401  subgintm  13406  nmzbi  13417  eqger  13432  eqgid  13434  eqgen  13435  qusgrp  13440  qusadd  13442  qusinv  13444  qussub  13445  ghminv  13458  ghmsub  13459  ghmrn  13465  resghm2b  13470  ghmf1  13481  conjsubg  13485  conjsubgen  13486  qusghm  13490  cmncom  13510  ablsubadd  13520  ablsubsub23  13533  ghmcmn  13535  gsumfzreidx  13545  mgpress  13565  srg1expzeq1  13629  ringinvnz1ne0  13683  ringinvnzdiv  13684  dvdsrd  13728  dvdsunit  13746  unitinvcl  13757  unitinvinv  13758  unitlinv  13760  unitrinv  13761  rhmunitinv  13812  subrngintm  13846  subrg1  13865  subrguss  13870  subrginv  13871  subrgunit  13873  subrgugrp  13874  subrgintm  13877  resrhm  13882  resrhm2b  13883  lmodass  13937  lmodlcan  13938  lmod0vlid  13952  lmod0vrid  13953  lmod0vid  13954  lmodvs0  13956  lcomf  13961  lmodvnegcl  13962  lmodvnegid  13963  lmodvsubadd  13972  lmodsubid  13981  lss1d  14017  lspval  14024  lspsnel6  14042  lspsnneg  14054  sralmod  14084  dflidl2rng  14115  lidlacl  14118  dflidl2  14122  df2idl2  14143  qusmul2  14163  quscrng  14167  cnfldmulg  14210  znf1o  14285  znidom  14291  psraddcl  14314  psr0lid  14316  tgss3  14422  clsval  14455  clsss3  14474  neiss2  14486  resttop  14514  resttopon2  14522  lmconst  14560  cnima  14564  cnntri  14568  cncnp  14574  cnrest  14579  cndis  14585  lmss  14590  lmff  14593  lmtopcnp  14594  txcnp  14615  upxp  14616  uptx  14618  cnmpt11  14627  hmeoima  14654  hmeoopn  14655  hmeocld  14656  hmeontr  14657  hmeoimaf1o  14658  mettri2  14706  met0  14708  metres2  14725  blpnf  14744  xblss2ps  14748  xblss2  14749  blbas  14777  blres  14778  xmetec  14781  mopnss  14794  xmstri2  14814  mstri2  14815  xmstri  14816  mstri  14817  xmstri3  14818  mstri3  14819  msrtri  14820  mopni3  14828  unimopn  14830  comet  14843  bdxmet  14845  climcncf  14928  dedekindeulemuub  14961  dedekindicclemuub  14970  ivthdichlem  14995  dvfgg  15032  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvfre  15054  dvmptfsum  15069  plyadd  15095  plymul  15096  reeff1olem  15115  reeff1o  15117  sinperlem  15152  abssinper  15190  reexplog  15215  relogexp  15216  cxpexpnn  15240  cxprec  15254  rpcxpmul2  15257  abscxp  15259  wilthlem1  15324  sgmval2  15328  sgmnncl  15332  0sgmppw  15337  perfectlem1  15343  lgsdir  15384  lgsprme0  15391  lgsdinn0  15397  gausslemma2dlem3  15412  gausslemma2dlem5a  15414  2lgslem1a2  15436  2lgslem1a  15437  2lgslem3  15450  2lgs  15453  bj-inex  15661  bj-nn0suc  15718  bj-nn0sucALT  15732  trilpolemeq1  15797  trilpolemlt1  15798  trirec0  15801  nconstwlpolemgt0  15821