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  947  dfifp2dc  990  3adantl1  1180  3adantl2  1181  3adantl3  1182  syl3anl1  1322  syl3anl3  1324  syl3anl  1325  stoic3  1476  eupick  2162  csbiebt  3181  csbnestgf  3194  reuss2  3505  mpteq12  4199  otexg  4352  opelopabt  4386  sonr  4444  sotr  4445  issod  4446  so2nr  4448  so3nr  4449  ordelss  4506  onelon  4511  elrnmpt1s  5014  iota2  5349  funeu  5384  imadif  5443  fnbr  5467  feu  5556  f1ss  5586  f1ssres  5589  f1resf1  5590  dffo2  5601  foco  5608  foun  5640  fun11iun  5642  ffoss  5654  funbrfv  5720  fvco3  5755  fvopab6  5781  funfvbrb  5798  elpreima  5804  ffvelcdm  5817  ffvelcdmda  5819  dffo4  5832  fmptco  5850  fsn2  5858  fncofn  5869  fvconst2g  5905  fex  5922  funfvima  5925  f1elima  5954  f1ocnvfv1  5958  f1ocnvfv2  5959  cocan2  5969  foeqcnvco  5971  isocnv  5992  isores2  5994  isoini  5999  isoselem  6001  f1oiso  6007  f1ofveu  6048  eloprabga  6150  suppssof1  6295  ofco  6296  offveqb  6297  ofc1g  6299  ofc2g  6300  caofid0l  6304  caofid0r  6305  caofid1  6306  caofid2  6307  fnexALT  6315  f1dmex  6320  ot1stg  6361  ot2ndg  6362  ot3rdgg  6363  eqopi  6381  2ndrn  6392  fo2ndf  6438  suppval1  6454  ressuppss  6469  suppssrst  6476  suppssrgst  6477  smores3  6539  smores2  6540  smoel  6546  smoiso  6548  tfrlem1  6554  tfrlemisucaccv  6571  tfrlemibxssdm  6573  tfrlemiubacc  6576  tfr1onlemsucaccv  6587  tfr1onlembfn  6590  tfr1onlemubacc  6592  tfr1onlemaccex  6594  tfr1onlemres  6595  tfrcllemsucaccv  6600  tfrcllembfn  6603  tfrcllemubacc  6605  tfrcllemaccex  6607  tfrcllemres  6608  tfrcl  6610  frecrdg  6654  omv2  6713  nnasuc  6724  nnmsuc  6725  nnacom  6732  nnaass  6733  nnmass  6735  nntri1  6744  nndifsnid  6755  nnmordi  6764  swoer  6810  erth  6828  riinerm  6857  qliftlem  6862  ecovass  6893  ecoviass  6894  elmapssres  6922  fvixp  6953  f1domg  7012  domssr  7032  endomtr  7045  xpsnen2g  7095  enen1  7108  enen2  7109  domen1  7110  domen2  7111  mapen  7114  mapxpen  7116  ssenen  7120  phplem1  7121  fidifsnid  7141  findcard  7160  findcard2  7161  findcard2s  7162  fidcen  7171  fieq0  7278  isotilem  7312  supisolem  7314  inflbti  7330  ordiso2  7341  djuex  7349  updjudhcoinlf  7386  updjudhcoinrg  7387  updjud  7388  ctssdccl  7417  enumctlemm  7420  nnnninf  7432  finomni  7446  pm54.43  7502  acfun  7529  ccfunen  7596  cc2lem  7598  cc3  7600  addclpi  7660  addasspig  7663  mulasspig  7665  addnidpig  7669  nnppipi  7676  ltanqi  7735  ltmnqi  7736  ltexnqq  7741  archnqq  7750  prarloclemarch2  7752  enq0sym  7765  enq0tr  7767  nqnq0pi  7771  nqnq0  7774  mulcanenq0ec  7778  addclnq0  7784  nqpnq0nq  7786  distrnq0  7792  addassnq0lemcl  7794  addassnq0  7795  prubl  7819  prarloclemlt  7826  genpdf  7841  genipv  7842  genpelvl  7845  genpelvu  7846  genpml  7850  genpmu  7851  genprndl  7854  genprndu  7855  genpassl  7857  genpassu  7858  genpassg  7859  addnqprl  7862  addnqpru  7863  addlocpr  7869  nqprm  7875  nqprl  7884  nqpru  7885  mulnqprl  7901  mulnqpru  7902  mullocprlem  7903  mullocpr  7904  addcomprg  7911  mulcomprg  7913  distrlem1prl  7915  distrlem1pru  7916  distrlem4prl  7917  distrlem4pru  7918  ltprordil  7922  1idprl  7923  1idpru  7924  ltpopr  7928  ltsopr  7929  ltaddpr  7930  ltexprlemm  7933  ltexprlemopl  7934  ltexprlemlol  7935  ltexprlemopu  7936  ltexprlemupu  7937  ltexprlemdisj  7939  ltexprlemloc  7940  ltexprlemfl  7942  ltexprlemrl  7943  ltexprlemfu  7944  ltexprlemru  7945  addcanprleml  7947  addcanprlemu  7948  prplnqu  7953  recexprlemloc  7964  recexprlem1ssl  7966  recexprlem1ssu  7967  recexprlemss1l  7968  recexprlemss1u  7969  aptiprleml  7972  aptiprlemu  7973  cauappcvgprlemloc  7985  cauappcvgprlemladdru  7989  cauappcvgprlemladdrl  7990  caucvgprlemloc  8008  caucvgprlemladdrl  8011  caucvgprprlemml  8027  caucvgprprlemloc  8036  00sr  8102  map2psrprg  8138  suplocsrlempr  8140  suplocsrlem  8141  adddir  8283  axsuploc  8364  eqle  8383  le2tri3i  8400  mul4  8424  muladd11  8425  cnegexlem3  8469  addsub12  8505  2addsub  8506  addsubeq4  8507  subadd4  8536  negcon1  8544  negdi2  8550  negsubdi2  8551  neg2sub  8552  renegcl  8553  muladd  8677  subdir  8679  gt0ne0  8721  ltnegcon1  8757  lenegcon1  8760  eqord1  8777  eqord2  8778  recexre  8872  ltmul1  8886  recexap  8947  div12ap  8990  rerecapb  9139  p1le  9145  ltmul2  9152  gt0div  9166  ge0div  9167  zlem1lt  9656  nnaddm1cl  9661  zdceq  9675  gtndiv  9696  prime  9700  msqznn  9701  btwnz  9720  uzss  9898  eluzadd  9906  nn0pzuz  9942  supinfneg  9950  infsupneg  9951  divfnzn  9976  qnegcl  9991  qreccl  9997  elpqb  10005  xaddass  10226  xleadd1a  10230  xlesubadd  10240  elico2  10294  iccss  10298  iccsupr  10323  elfz5  10375  fznn  10450  difelfznle  10496  fzoaddel  10559  elincfzoext  10565  qdceq  10633  qbtwnxr  10646  flqbi2  10680  adddivflid  10681  fldivnn0  10684  divfl0  10685  flqmulnn0  10688  fldivnn0le  10692  fldiv4p1lem1div2  10694  ceiqle  10704  flqdiv  10712  modqmulnn  10733  frecuzrdgtcl  10803  frecuzrdgsuc  10805  frecuzrdgdomlem  10808  frecuzrdgfunlem  10810  frecuzrdgsuctlem  10814  seqm1g  10865  seq3caopr2  10884  seqcaopr2g  10885  iseqf1olemkle  10888  seq3f1olemp  10906  seqf1oglem2  10911  seqf1og  10912  seq3id  10916  seq3z  10919  expap0  10960  mulexp  10969  mulexpzap  10970  expmul  10975  leexp1a  10985  expubnd  10987  zesq  11050  bernneq  11052  bernneq3  11054  modqexp  11058  facdiv  11130  facndiv  11131  faclbnd3  11135  faclbnd6  11136  bccmpl  11146  bcpasc  11158  bccl  11159  hashfibclem  11236  hashfibc  11237  seq3coll  11244  fundm2domnop  11251  wrdsymb1  11291  ccatfv0  11321  ccatrn  11327  ccat2s1cl  11351  lswccats1fst  11362  swrdspsleq  11389  pfxtrcfv  11415  pfxsuffeqwrdeq  11420  pfxlswccat  11435  wrdeqs1cat  11442  cats1un  11443  swrdccatin1  11447  pfxccatin12lem4  11448  swrdccatin2  11451  pfxccatin12  11455  swrdccat  11457  shftlem  11531  ovshftex  11534  shftval4  11543  shftf  11545  shftcan2  11550  crim  11573  mulreap  11579  remul2  11588  immul2  11595  cjexp  11608  caucvgre  11697  r19.2uz  11709  sqrtsq2  11759  absnid  11789  absexp  11795  nn0abscl  11801  abslt  11804  lenegsq  11811  cau3lem  11830  minmax  11946  xrmaxadd  11977  clim  11997  climshftlemg  12018  climcn1  12024  climcn1lem  12035  clim2ser  12053  clim2ser2  12054  iserex  12055  isermulc2  12056  climub  12060  climcaucn  12067  serf0  12068  summodclem3  12097  summodclem2a  12098  summodclem2  12099  summodc  12100  fsum3  12104  fsumf1o  12107  fisumss  12109  isumss2  12110  fsumcl2lem  12115  fsumadd  12123  fsumsplit  12124  isummulc2  12143  fsum2d  12152  fsummulc2  12165  telfsumo  12183  fsumparts  12187  hash2iun1dif1  12197  bcxmas  12206  isumshft  12207  isumsplit  12208  expcnvap0  12219  geolim  12228  geolim2  12229  cvgratnnlemmn  12242  cvgratnnlemseq  12243  mertenslemi1  12252  mertenslem2  12253  mertensabs  12254  clim2divap  12257  prodmodclem3  12292  prodmodclem2a  12293  fprodseq  12300  fprodf1o  12305  fprodmul  12308  fprodsplitdc  12313  efcllemp  12375  reefcl  12385  efcj  12390  efaddlem  12391  efexp  12399  reeftlcl  12406  eftlub  12407  efsep  12408  effsumlt  12409  eflegeo  12418  retanclap  12439  demoivre  12490  demoivreALT  12491  eirraplem  12494  dvdsval3  12508  p1modz1  12511  iddvdsexp  12532  alzdvds  12571  addmodlteqALT  12576  nnehalf  12621  nno  12623  ndvdsadd  12648  bitsp1e  12669  bitsp1o  12670  bitsinv1  12679  divgcdnnr  12703  neggcd  12710  gcdabs  12715  bezoutlemmain  12725  bezoutlemaz  12730  bezoutlembz  12731  gcdmultiplez  12748  gcdzeq  12749  dvdssq  12758  nninfctlemfo  12767  algrf  12773  algcvg  12776  algcvga  12779  algfx  12780  eucalgf  12783  eucalgcvga  12786  neglcm  12803  lcmabs  12804  lcmdvds  12807  lcmgcdeq  12811  qredeq  12824  isprm3  12846  coprm  12872  prmrp  12873  isprm6  12875  prmdvdsexpb  12877  rpexp  12881  cncongrprm  12885  sqrt2irraplemnn  12907  phibndlem  12944  phiprmpw  12950  eulerthlemh  12959  eulerthlemth  12960  fermltl  12962  prmdivdiv  12965  modprm1div  12976  m1dvdsndvds  12977  coprimeprodsq  12986  pczpre  13026  pczcl  13027  pcexp  13038  pczdvds  13043  pczndvds  13045  pczndvds2  13047  pcdvdsb  13049  pcneg  13054  pcprmpw  13063  difsqpwdvds  13067  pcmptcl  13071  pcprod  13075  fldivp1  13077  infpnlem2  13089  1arithlem4  13095  ballotfilem2  13178  ballotfilemfc0  13182  ballotfilemfcc  13183  ballotfilemfrcn0  13223  ennnfonelemrn  13260  topnidg  13555  imasaddfnlemg  13584  imasaddflemg  13586  qusin  13596  mgmlrid  13648  mndass  13691  mhmco  13751  gsumsubm  13755  gsumwcl  13758  gsumwmhm  13759  grpass  13770  grpinvex  13771  dfgrp2  13788  grplid  13792  grprid  13793  grprcan  13798  grpinvssd  13838  grpinvval2  13844  mhmid  13874  mhmmnd  13875  ghmgrp  13877  mulgnn  13885  mulgnnp1  13889  mulgnegnn  13891  mulgnnsubcl  13893  mulgz  13909  issubg2m  13948  issubg4m  13952  subgintm  13957  nmzbi  13968  eqger  13983  eqgid  13985  eqgen  13986  qusgrp  13991  qusadd  13993  qusinv  13995  qussub  13996  ghminv  14009  ghmsub  14010  ghmrn  14016  resghm2b  14021  ghmf1  14032  conjsubg  14036  conjsubgen  14037  qusghm  14041  cmncom  14061  ablsubadd  14071  ablsubsub23  14084  ghmcmn  14086  gsumfzreidx  14096  prdsidlem  14141  prdsinvlem  14144  pwselbasb  14154  pwsplusgval  14156  pwsmulrval  14157  pwsinvg  14163  mgpress  14176  srg1expzeq1  14244  ringinvnz1ne0  14298  ringinvnzdiv  14299  dvdsrd  14345  dvdsunit  14363  unitinvcl  14374  unitinvinv  14375  unitlinv  14377  unitrinv  14378  rhmunitinv  14429  subrngintm  14464  subrg1  14483  subrguss  14488  subrginv  14489  subrgunit  14491  subrgugrp  14492  subrgintm  14495  resrhm  14500  resrhm2b  14501  lmodass  14583  lmodlcan  14584  lmod0vlid  14598  lmod0vrid  14599  lmod0vid  14600  lmodvs0  14602  lcomf  14607  lmodvnegcl  14608  lmodvnegid  14609  lmodvsubadd  14618  lmodsubid  14627  lss1d  14663  lspval  14670  lspsnel6  14688  lspsnneg  14700  sralmod  14730  dflidl2rng  14761  lidlacl  14764  dflidl2  14768  df2idl2  14789  qusmul2  14809  quscrng  14813  cnfldmulg  14856  znf1o  14931  znidom  14937  psraddcl  14967  psr0lid  14969  tgss3  15075  clsval  15108  clsss3  15127  neiss2  15139  resttop  15167  resttopon2  15175  lmconst  15213  cnima  15217  cnntri  15221  cncnp  15227  cnrest  15232  cndis  15238  lmss  15243  lmff  15246  lmtopcnp  15247  txcnp  15268  upxp  15269  uptx  15271  cnmpt11  15280  hmeoima  15307  hmeoopn  15308  hmeocld  15309  hmeontr  15310  hmeoimaf1o  15311  mettri2  15359  met0  15361  metres2  15378  blpnf  15397  xblss2ps  15401  xblss2  15402  blbas  15430  blres  15431  xmetec  15434  mopnss  15447  xmstri2  15467  mstri2  15468  xmstri  15469  mstri  15470  xmstri3  15471  mstri3  15472  msrtri  15473  mopni3  15481  unimopn  15483  comet  15496  bdxmet  15498  climcncf  15581  dedekindeulemuub  15614  dedekindicclemuub  15623  ivthdichlem  15648  dvfgg  15685  dvidlemap  15688  dvidrelem  15689  dvidsslem  15690  dvfre  15707  dvmptfsum  15722  plyadd  15748  plymul  15749  reeff1olem  15768  reeff1o  15770  sinperlem  15805  abssinper  15843  reexplog  15868  relogexp  15869  cxpexpnn  15893  cxprec  15907  rpcxpmul2  15910  abscxp  15912  wilthlem1  15980  sgmval2  15984  sgmnncl  15988  0sgmppw  15993  perfectlem1  15999  lgsdir  16040  lgsprme0  16047  lgsdinn0  16053  gausslemma2dlem3  16068  gausslemma2dlem5a  16070  2lgslem1a2  16092  2lgslem1a  16093  2lgslem3  16106  2lgs  16109  umgredgprv  16242  umgrislfupgrdom  16258  uspgredgiedg  16305  uspgriedgedg  16306  usgrislfuspgrdom  16317  usgredg2en  16322  usgredgprv  16323  usgrpredgv  16325  usgredg  16327  usgrnloopv  16328  usgredgne  16331  usgredg3  16341  usgredgedg  16354  usgredgdomord  16357  usgr1vr  16375  subgruhgrfun  16395  subupgr  16400  subumgr  16401  subusgr  16402  umgrwlknloop  16495  wlkres  16506  clwwlkccatlem  16527  clwwlkccat  16528  depindlem1  16633  depindlem2  16634  depindlem3  16635  bj-inex  16819  bj-nn0suc  16876  bj-nn0sucALT  16890  trilpolemeq1  16966  trilpolemlt1  16967  trirec0  16970  nconstwlpolemgt0  16991