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  944  dfifp2dc  987  3adantl1  1177  3adantl2  1178  3adantl3  1179  syl3anl1  1319  syl3anl3  1321  syl3anl  1322  stoic3  1473  eupick  2157  csbiebt  3164  csbnestgf  3177  reuss2  3484  mpteq12  4167  otexg  4317  opelopabt  4351  sonr  4409  sotr  4410  issod  4411  so2nr  4413  so3nr  4414  ordelss  4471  onelon  4476  elrnmpt1s  4977  iota2  5311  funeu  5346  imadif  5404  fnbr  5428  feu  5513  f1ss  5542  f1ssres  5545  f1resf1  5546  dffo2  5557  foco  5564  foun  5596  fun11iun  5598  ffoss  5609  funbrfv  5675  fvco3  5710  fvopab6  5736  funfvbrb  5753  elpreima  5759  ffvelcdm  5773  ffvelcdmda  5775  dffo4  5788  fmptco  5806  fsn2  5814  fncofn  5824  fvconst2g  5860  fex  5875  funfvima  5878  f1elima  5906  f1ocnvfv1  5910  f1ocnvfv2  5911  cocan2  5921  foeqcnvco  5923  isocnv  5944  isores2  5946  isoini  5951  isoselem  5953  f1oiso  5959  f1ofveu  5998  eloprabga  6100  suppssof1  6245  ofco  6246  offveqb  6247  ofc1g  6249  ofc2g  6250  caofid0l  6254  caofid0r  6255  caofid1  6256  caofid2  6257  fnexALT  6265  f1dmex  6270  ot1stg  6307  ot2ndg  6308  ot3rdgg  6309  eqopi  6327  2ndrn  6338  fo2ndf  6384  smores3  6450  smores2  6451  smoel  6457  smoiso  6459  tfrlem1  6465  tfrlemisucaccv  6482  tfrlemibxssdm  6484  tfrlemiubacc  6487  tfr1onlemsucaccv  6498  tfr1onlembfn  6501  tfr1onlemubacc  6503  tfr1onlemaccex  6505  tfr1onlemres  6506  tfrcllemsucaccv  6511  tfrcllembfn  6514  tfrcllemubacc  6516  tfrcllemaccex  6518  tfrcllemres  6519  tfrcl  6521  frecrdg  6565  omv2  6624  nnasuc  6635  nnmsuc  6636  nnacom  6643  nnaass  6644  nnmass  6646  nntri1  6655  nndifsnid  6666  nnmordi  6675  swoer  6721  erth  6739  riinerm  6768  qliftlem  6773  ecovass  6804  ecoviass  6805  elmapssres  6833  fvixp  6863  f1domg  6922  domssr  6942  endomtr  6955  xpsnen2g  7001  enen1  7014  enen2  7015  domen1  7016  domen2  7017  mapen  7020  mapxpen  7022  ssenen  7025  phplem1  7026  fidifsnid  7046  findcard  7063  findcard2  7064  findcard2s  7065  fidcen  7074  fieq0  7159  isotilem  7189  supisolem  7191  inflbti  7207  ordiso2  7218  djuex  7226  updjudhcoinlf  7263  updjudhcoinrg  7264  updjud  7265  ctssdccl  7294  enumctlemm  7297  nnnninf  7309  finomni  7323  pm54.43  7379  acfun  7405  ccfunen  7466  cc2lem  7468  cc3  7470  addclpi  7530  addasspig  7533  mulasspig  7535  addnidpig  7539  nnppipi  7546  ltanqi  7605  ltmnqi  7606  ltexnqq  7611  archnqq  7620  prarloclemarch2  7622  enq0sym  7635  enq0tr  7637  nqnq0pi  7641  nqnq0  7644  mulcanenq0ec  7648  addclnq0  7654  nqpnq0nq  7656  distrnq0  7662  addassnq0lemcl  7664  addassnq0  7665  prubl  7689  prarloclemlt  7696  genpdf  7711  genipv  7712  genpelvl  7715  genpelvu  7716  genpml  7720  genpmu  7721  genprndl  7724  genprndu  7725  genpassl  7727  genpassu  7728  genpassg  7729  addnqprl  7732  addnqpru  7733  addlocpr  7739  nqprm  7745  nqprl  7754  nqpru  7755  mulnqprl  7771  mulnqpru  7772  mullocprlem  7773  mullocpr  7774  addcomprg  7781  mulcomprg  7783  distrlem1prl  7785  distrlem1pru  7786  distrlem4prl  7787  distrlem4pru  7788  ltprordil  7792  1idprl  7793  1idpru  7794  ltpopr  7798  ltsopr  7799  ltaddpr  7800  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemlol  7805  ltexprlemopu  7806  ltexprlemupu  7807  ltexprlemdisj  7809  ltexprlemloc  7810  ltexprlemfl  7812  ltexprlemrl  7813  ltexprlemfu  7814  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  prplnqu  7823  recexprlemloc  7834  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1l  7838  recexprlemss1u  7839  aptiprleml  7842  aptiprlemu  7843  cauappcvgprlemloc  7855  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  caucvgprlemloc  7878  caucvgprlemladdrl  7881  caucvgprprlemml  7897  caucvgprprlemloc  7906  00sr  7972  map2psrprg  8008  suplocsrlempr  8010  suplocsrlem  8011  adddir  8153  axsuploc  8235  eqle  8254  le2tri3i  8271  mul4  8294  muladd11  8295  cnegexlem3  8339  addsub12  8375  2addsub  8376  addsubeq4  8377  subadd4  8406  negcon1  8414  negdi2  8420  negsubdi2  8421  neg2sub  8422  renegcl  8423  muladd  8546  subdir  8548  gt0ne0  8590  ltnegcon1  8626  lenegcon1  8629  eqord1  8646  eqord2  8647  recexre  8741  ltmul1  8755  recexap  8816  div12ap  8857  rerecapb  9006  p1le  9012  ltmul2  9019  gt0div  9033  ge0div  9034  zlem1lt  9519  nnaddm1cl  9524  zdceq  9538  gtndiv  9558  prime  9562  msqznn  9563  btwnz  9582  uzss  9760  eluzadd  9768  nn0pzuz  9799  supinfneg  9807  infsupneg  9808  divfnzn  9833  qnegcl  9848  qreccl  9854  elpqb  9862  xaddass  10082  xleadd1a  10086  xlesubadd  10096  elico2  10150  iccss  10154  iccsupr  10179  elfz5  10230  fznn  10302  difelfznle  10348  fzoaddel  10410  elincfzoext  10416  qdceq  10481  qbtwnxr  10494  flqbi2  10528  adddivflid  10529  fldivnn0  10532  divfl0  10533  flqmulnn0  10536  fldivnn0le  10540  fldiv4p1lem1div2  10542  ceiqle  10552  flqdiv  10560  modqmulnn  10581  frecuzrdgtcl  10651  frecuzrdgsuc  10653  frecuzrdgdomlem  10656  frecuzrdgfunlem  10658  frecuzrdgsuctlem  10662  seqm1g  10713  seq3caopr2  10732  seqcaopr2g  10733  iseqf1olemkle  10736  seq3f1olemp  10754  seqf1oglem2  10759  seqf1og  10760  seq3id  10764  seq3z  10767  expap0  10808  mulexp  10817  mulexpzap  10818  expmul  10823  leexp1a  10833  expubnd  10835  zesq  10897  bernneq  10899  bernneq3  10901  modqexp  10905  facdiv  10977  facndiv  10978  faclbnd3  10982  faclbnd6  10983  bccmpl  10993  bcpasc  11005  bccl  11006  seq3coll  11082  fundm2domnop  11086  wrdsymb1  11126  ccatfv0  11156  ccatrn  11162  ccat2s1cl  11186  lswccats1fst  11196  swrdspsleq  11220  pfxtrcfv  11246  pfxsuffeqwrdeq  11251  pfxlswccat  11266  wrdeqs1cat  11273  cats1un  11274  swrdccatin1  11278  pfxccatin12lem4  11279  swrdccatin2  11282  pfxccatin12  11286  swrdccat  11288  shftlem  11348  ovshftex  11351  shftval4  11360  shftf  11362  shftcan2  11367  crim  11390  mulreap  11396  remul2  11405  immul2  11412  cjexp  11425  caucvgre  11513  r19.2uz  11525  sqrtsq2  11575  absnid  11605  absexp  11611  nn0abscl  11617  abslt  11620  lenegsq  11627  cau3lem  11646  minmax  11762  xrmaxadd  11793  clim  11813  climshftlemg  11834  climcn1  11840  climcn1lem  11851  clim2ser  11869  clim2ser2  11870  iserex  11871  isermulc2  11872  climub  11876  climcaucn  11883  serf0  11884  summodclem3  11912  summodclem2a  11913  summodclem2  11914  summodc  11915  fsum3  11919  fsumf1o  11922  fisumss  11924  isumss2  11925  fsumcl2lem  11930  fsumadd  11938  fsumsplit  11939  isummulc2  11958  fsum2d  11967  fsummulc2  11980  telfsumo  11998  fsumparts  12002  hash2iun1dif1  12012  bcxmas  12021  isumshft  12022  isumsplit  12023  expcnvap0  12034  geolim  12043  geolim2  12044  cvgratnnlemmn  12057  cvgratnnlemseq  12058  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  clim2divap  12072  prodmodclem3  12107  prodmodclem2a  12108  fprodseq  12115  fprodf1o  12120  fprodmul  12123  fprodsplitdc  12128  efcllemp  12190  reefcl  12200  efcj  12205  efaddlem  12206  efexp  12214  reeftlcl  12221  eftlub  12222  efsep  12223  effsumlt  12224  eflegeo  12233  retanclap  12254  demoivre  12305  demoivreALT  12306  eirraplem  12309  dvdsval3  12323  p1modz1  12326  iddvdsexp  12347  alzdvds  12386  addmodlteqALT  12391  nnehalf  12436  nno  12438  ndvdsadd  12463  bitsp1e  12484  bitsp1o  12485  bitsinv1  12494  divgcdnnr  12518  neggcd  12525  gcdabs  12530  bezoutlemmain  12540  bezoutlemaz  12545  bezoutlembz  12546  gcdmultiplez  12563  gcdzeq  12564  dvdssq  12573  nninfctlemfo  12582  algrf  12588  algcvg  12591  algcvga  12594  algfx  12595  eucalgf  12598  eucalgcvga  12601  neglcm  12618  lcmabs  12619  lcmdvds  12622  lcmgcdeq  12626  qredeq  12639  isprm3  12661  coprm  12687  prmrp  12688  isprm6  12690  prmdvdsexpb  12692  rpexp  12696  cncongrprm  12700  sqrt2irraplemnn  12722  phibndlem  12759  phiprmpw  12765  eulerthlemh  12774  eulerthlemth  12775  fermltl  12777  prmdivdiv  12780  modprm1div  12791  m1dvdsndvds  12792  coprimeprodsq  12801  pczpre  12841  pczcl  12842  pcexp  12853  pczdvds  12858  pczndvds  12860  pczndvds2  12862  pcdvdsb  12864  pcneg  12869  pcprmpw  12878  difsqpwdvds  12882  pcmptcl  12886  pcprod  12890  fldivp1  12892  infpnlem2  12904  1arithlem4  12910  ennnfonelemrn  13011  topnidg  13306  pwselbasb  13347  pwsplusgval  13349  pwsmulrval  13350  imasaddfnlemg  13368  imasaddflemg  13370  qusin  13380  mgmlrid  13433  mndass  13478  prdsidlem  13501  mhmco  13544  gsumsubm  13548  gsumwcl  13551  gsumwmhm  13552  grpass  13563  grpinvex  13564  dfgrp2  13581  grplid  13585  grprid  13586  grprcan  13591  grpinvssd  13631  grpinvval2  13637  prdsinvlem  13662  pwsinvg  13666  mhmid  13673  mhmmnd  13674  ghmgrp  13676  mulgnn  13684  mulgnnp1  13688  mulgnegnn  13690  mulgnnsubcl  13692  mulgz  13708  issubg2m  13747  issubg4m  13751  subgintm  13756  nmzbi  13767  eqger  13782  eqgid  13784  eqgen  13785  qusgrp  13790  qusadd  13792  qusinv  13794  qussub  13795  ghminv  13808  ghmsub  13809  ghmrn  13815  resghm2b  13820  ghmf1  13831  conjsubg  13835  conjsubgen  13836  qusghm  13840  cmncom  13860  ablsubadd  13870  ablsubsub23  13883  ghmcmn  13885  gsumfzreidx  13895  mgpress  13915  srg1expzeq1  13979  ringinvnz1ne0  14033  ringinvnzdiv  14034  dvdsrd  14079  dvdsunit  14097  unitinvcl  14108  unitinvinv  14109  unitlinv  14111  unitrinv  14112  rhmunitinv  14163  subrngintm  14197  subrg1  14216  subrguss  14221  subrginv  14222  subrgunit  14224  subrgugrp  14225  subrgintm  14228  resrhm  14233  resrhm2b  14234  lmodass  14288  lmodlcan  14289  lmod0vlid  14303  lmod0vrid  14304  lmod0vid  14305  lmodvs0  14307  lcomf  14312  lmodvnegcl  14313  lmodvnegid  14314  lmodvsubadd  14323  lmodsubid  14332  lss1d  14368  lspval  14375  lspsnel6  14393  lspsnneg  14405  sralmod  14435  dflidl2rng  14466  lidlacl  14469  dflidl2  14473  df2idl2  14494  qusmul2  14514  quscrng  14518  cnfldmulg  14561  znf1o  14636  znidom  14642  psraddcl  14665  psr0lid  14667  tgss3  14773  clsval  14806  clsss3  14825  neiss2  14837  resttop  14865  resttopon2  14873  lmconst  14911  cnima  14915  cnntri  14919  cncnp  14925  cnrest  14930  cndis  14936  lmss  14941  lmff  14944  lmtopcnp  14945  txcnp  14966  upxp  14967  uptx  14969  cnmpt11  14978  hmeoima  15005  hmeoopn  15006  hmeocld  15007  hmeontr  15008  hmeoimaf1o  15009  mettri2  15057  met0  15059  metres2  15076  blpnf  15095  xblss2ps  15099  xblss2  15100  blbas  15128  blres  15129  xmetec  15132  mopnss  15145  xmstri2  15165  mstri2  15166  xmstri  15167  mstri  15168  xmstri3  15169  mstri3  15170  msrtri  15171  mopni3  15179  unimopn  15181  comet  15194  bdxmet  15196  climcncf  15279  dedekindeulemuub  15312  dedekindicclemuub  15321  ivthdichlem  15346  dvfgg  15383  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvfre  15405  dvmptfsum  15420  plyadd  15446  plymul  15447  reeff1olem  15466  reeff1o  15468  sinperlem  15503  abssinper  15541  reexplog  15566  relogexp  15567  cxpexpnn  15591  cxprec  15605  rpcxpmul2  15608  abscxp  15610  wilthlem1  15675  sgmval2  15679  sgmnncl  15683  0sgmppw  15688  perfectlem1  15694  lgsdir  15735  lgsprme0  15742  lgsdinn0  15748  gausslemma2dlem3  15763  gausslemma2dlem5a  15765  2lgslem1a2  15787  2lgslem1a  15788  2lgslem3  15801  2lgs  15804  umgredgprv  15936  umgrislfupgrdom  15950  uspgredgiedg  15997  uspgriedgedg  15998  usgrislfuspgrdom  16009  usgredg2en  16014  usgredgprv  16015  usgrpredgv  16017  usgredg  16019  usgrnloopv  16020  usgredgne  16023  usgredg3  16033  usgredgedg  16046  usgredgdomord  16049  usgr1vr  16067  umgrwlknloop  16140  wlkres  16149  clwwlkccatlem  16169  clwwlkccat  16170  bj-inex  16379  bj-nn0suc  16436  bj-nn0sucALT  16450  trilpolemeq1  16522  trilpolemlt1  16523  trirec0  16526  nconstwlpolemgt0  16546