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  2159  csbiebt  3168  csbnestgf  3181  reuss2  3489  mpteq12  4177  otexg  4328  opelopabt  4362  sonr  4420  sotr  4421  issod  4422  so2nr  4424  so3nr  4425  ordelss  4482  onelon  4487  elrnmpt1s  4988  iota2  5323  funeu  5358  imadif  5417  fnbr  5441  feu  5527  f1ss  5557  f1ssres  5560  f1resf1  5561  dffo2  5572  foco  5579  foun  5611  fun11iun  5613  ffoss  5625  funbrfv  5691  fvco3  5726  fvopab6  5752  funfvbrb  5769  elpreima  5775  ffvelcdm  5788  ffvelcdmda  5790  dffo4  5803  fmptco  5821  fsn2  5829  fncofn  5840  fvconst2g  5876  fex  5893  funfvima  5896  f1elima  5924  f1ocnvfv1  5928  f1ocnvfv2  5929  cocan2  5939  foeqcnvco  5941  isocnv  5962  isores2  5964  isoini  5969  isoselem  5971  f1oiso  5977  f1ofveu  6016  eloprabga  6118  suppssof1  6262  ofco  6263  offveqb  6264  ofc1g  6266  ofc2g  6267  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  fnexALT  6282  f1dmex  6287  ot1stg  6324  ot2ndg  6325  ot3rdgg  6326  eqopi  6344  2ndrn  6355  fo2ndf  6401  suppval1  6417  ressuppss  6432  suppssrst  6439  suppssrgst  6440  smores3  6502  smores2  6503  smoel  6509  smoiso  6511  tfrlem1  6517  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemiubacc  6539  tfr1onlemsucaccv  6550  tfr1onlembfn  6553  tfr1onlemubacc  6555  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembfn  6566  tfrcllemubacc  6568  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  frecrdg  6617  omv2  6676  nnasuc  6687  nnmsuc  6688  nnacom  6695  nnaass  6696  nnmass  6698  nntri1  6707  nndifsnid  6718  nnmordi  6727  swoer  6773  erth  6791  riinerm  6820  qliftlem  6825  ecovass  6856  ecoviass  6857  elmapssres  6885  fvixp  6915  f1domg  6974  domssr  6994  endomtr  7007  xpsnen2g  7056  enen1  7069  enen2  7070  domen1  7071  domen2  7072  mapen  7075  mapxpen  7077  ssenen  7080  phplem1  7081  fidifsnid  7101  findcard  7120  findcard2  7121  findcard2s  7122  fidcen  7131  fieq0  7218  isotilem  7248  supisolem  7250  inflbti  7266  ordiso2  7277  djuex  7285  updjudhcoinlf  7322  updjudhcoinrg  7323  updjud  7324  ctssdccl  7353  enumctlemm  7356  nnnninf  7368  finomni  7382  pm54.43  7438  acfun  7465  ccfunen  7526  cc2lem  7528  cc3  7530  addclpi  7590  addasspig  7593  mulasspig  7595  addnidpig  7599  nnppipi  7606  ltanqi  7665  ltmnqi  7666  ltexnqq  7671  archnqq  7680  prarloclemarch2  7682  enq0sym  7695  enq0tr  7697  nqnq0pi  7701  nqnq0  7704  mulcanenq0ec  7708  addclnq0  7714  nqpnq0nq  7716  distrnq0  7722  addassnq0lemcl  7724  addassnq0  7725  prubl  7749  prarloclemlt  7756  genpdf  7771  genipv  7772  genpelvl  7775  genpelvu  7776  genpml  7780  genpmu  7781  genprndl  7784  genprndu  7785  genpassl  7787  genpassu  7788  genpassg  7789  addnqprl  7792  addnqpru  7793  addlocpr  7799  nqprm  7805  nqprl  7814  nqpru  7815  mulnqprl  7831  mulnqpru  7832  mullocprlem  7833  mullocpr  7834  addcomprg  7841  mulcomprg  7843  distrlem1prl  7845  distrlem1pru  7846  distrlem4prl  7847  distrlem4pru  7848  ltprordil  7852  1idprl  7853  1idpru  7854  ltpopr  7858  ltsopr  7859  ltaddpr  7860  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  prplnqu  7883  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1l  7898  recexprlemss1u  7899  aptiprleml  7902  aptiprlemu  7903  cauappcvgprlemloc  7915  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemloc  7938  caucvgprlemladdrl  7941  caucvgprprlemml  7957  caucvgprprlemloc  7966  00sr  8032  map2psrprg  8068  suplocsrlempr  8070  suplocsrlem  8071  adddir  8213  axsuploc  8295  eqle  8314  le2tri3i  8331  mul4  8354  muladd11  8355  cnegexlem3  8399  addsub12  8435  2addsub  8436  addsubeq4  8437  subadd4  8466  negcon1  8474  negdi2  8480  negsubdi2  8481  neg2sub  8482  renegcl  8483  muladd  8606  subdir  8608  gt0ne0  8650  ltnegcon1  8686  lenegcon1  8689  eqord1  8706  eqord2  8707  recexre  8801  ltmul1  8815  recexap  8876  div12ap  8917  rerecapb  9066  p1le  9072  ltmul2  9079  gt0div  9093  ge0div  9094  zlem1lt  9579  nnaddm1cl  9584  zdceq  9598  gtndiv  9618  prime  9622  msqznn  9623  btwnz  9642  uzss  9820  eluzadd  9828  nn0pzuz  9864  supinfneg  9872  infsupneg  9873  divfnzn  9898  qnegcl  9913  qreccl  9919  elpqb  9927  xaddass  10147  xleadd1a  10151  xlesubadd  10161  elico2  10215  iccss  10219  iccsupr  10244  elfz5  10295  fznn  10367  difelfznle  10413  fzoaddel  10476  elincfzoext  10482  qdceq  10548  qbtwnxr  10561  flqbi2  10595  adddivflid  10596  fldivnn0  10599  divfl0  10600  flqmulnn0  10603  fldivnn0le  10607  fldiv4p1lem1div2  10609  ceiqle  10619  flqdiv  10627  modqmulnn  10648  frecuzrdgtcl  10718  frecuzrdgsuc  10720  frecuzrdgdomlem  10723  frecuzrdgfunlem  10725  frecuzrdgsuctlem  10729  seqm1g  10780  seq3caopr2  10799  seqcaopr2g  10800  iseqf1olemkle  10803  seq3f1olemp  10821  seqf1oglem2  10826  seqf1og  10827  seq3id  10831  seq3z  10834  expap0  10875  mulexp  10884  mulexpzap  10885  expmul  10890  leexp1a  10900  expubnd  10902  zesq  10964  bernneq  10966  bernneq3  10968  modqexp  10972  facdiv  11044  facndiv  11045  faclbnd3  11049  faclbnd6  11050  bccmpl  11060  bcpasc  11072  bccl  11073  seq3coll  11150  fundm2domnop  11157  wrdsymb1  11197  ccatfv0  11227  ccatrn  11233  ccat2s1cl  11257  lswccats1fst  11268  swrdspsleq  11295  pfxtrcfv  11321  pfxsuffeqwrdeq  11326  pfxlswccat  11341  wrdeqs1cat  11348  cats1un  11349  swrdccatin1  11353  pfxccatin12lem4  11354  swrdccatin2  11357  pfxccatin12  11361  swrdccat  11363  shftlem  11437  ovshftex  11440  shftval4  11449  shftf  11451  shftcan2  11456  crim  11479  mulreap  11485  remul2  11494  immul2  11501  cjexp  11514  caucvgre  11602  r19.2uz  11614  sqrtsq2  11664  absnid  11694  absexp  11700  nn0abscl  11706  abslt  11709  lenegsq  11716  cau3lem  11735  minmax  11851  xrmaxadd  11882  clim  11902  climshftlemg  11923  climcn1  11929  climcn1lem  11940  clim2ser  11958  clim2ser2  11959  iserex  11960  isermulc2  11961  climub  11965  climcaucn  11972  serf0  11973  summodclem3  12002  summodclem2a  12003  summodclem2  12004  summodc  12005  fsum3  12009  fsumf1o  12012  fisumss  12014  isumss2  12015  fsumcl2lem  12020  fsumadd  12028  fsumsplit  12029  isummulc2  12048  fsum2d  12057  fsummulc2  12070  telfsumo  12088  fsumparts  12092  hash2iun1dif1  12102  bcxmas  12111  isumshft  12112  isumsplit  12113  expcnvap0  12124  geolim  12133  geolim2  12134  cvgratnnlemmn  12147  cvgratnnlemseq  12148  mertenslemi1  12157  mertenslem2  12158  mertensabs  12159  clim2divap  12162  prodmodclem3  12197  prodmodclem2a  12198  fprodseq  12205  fprodf1o  12210  fprodmul  12213  fprodsplitdc  12218  efcllemp  12280  reefcl  12290  efcj  12295  efaddlem  12296  efexp  12304  reeftlcl  12311  eftlub  12312  efsep  12313  effsumlt  12314  eflegeo  12323  retanclap  12344  demoivre  12395  demoivreALT  12396  eirraplem  12399  dvdsval3  12413  p1modz1  12416  iddvdsexp  12437  alzdvds  12476  addmodlteqALT  12481  nnehalf  12526  nno  12528  ndvdsadd  12553  bitsp1e  12574  bitsp1o  12575  bitsinv1  12584  divgcdnnr  12608  neggcd  12615  gcdabs  12620  bezoutlemmain  12630  bezoutlemaz  12635  bezoutlembz  12636  gcdmultiplez  12653  gcdzeq  12654  dvdssq  12663  nninfctlemfo  12672  algrf  12678  algcvg  12681  algcvga  12684  algfx  12685  eucalgf  12688  eucalgcvga  12691  neglcm  12708  lcmabs  12709  lcmdvds  12712  lcmgcdeq  12716  qredeq  12729  isprm3  12751  coprm  12777  prmrp  12778  isprm6  12780  prmdvdsexpb  12782  rpexp  12786  cncongrprm  12790  sqrt2irraplemnn  12812  phibndlem  12849  phiprmpw  12855  eulerthlemh  12864  eulerthlemth  12865  fermltl  12867  prmdivdiv  12870  modprm1div  12881  m1dvdsndvds  12882  coprimeprodsq  12891  pczpre  12931  pczcl  12932  pcexp  12943  pczdvds  12948  pczndvds  12950  pczndvds2  12952  pcdvdsb  12954  pcneg  12959  pcprmpw  12968  difsqpwdvds  12972  pcmptcl  12976  pcprod  12980  fldivp1  12982  infpnlem2  12994  1arithlem4  13000  ennnfonelemrn  13101  topnidg  13396  pwselbasb  13437  pwsplusgval  13439  pwsmulrval  13440  imasaddfnlemg  13458  imasaddflemg  13460  qusin  13470  mgmlrid  13523  mndass  13568  prdsidlem  13591  mhmco  13634  gsumsubm  13638  gsumwcl  13641  gsumwmhm  13642  grpass  13653  grpinvex  13654  dfgrp2  13671  grplid  13675  grprid  13676  grprcan  13681  grpinvssd  13721  grpinvval2  13727  prdsinvlem  13752  pwsinvg  13756  mhmid  13763  mhmmnd  13764  ghmgrp  13766  mulgnn  13774  mulgnnp1  13778  mulgnegnn  13780  mulgnnsubcl  13782  mulgz  13798  issubg2m  13837  issubg4m  13841  subgintm  13846  nmzbi  13857  eqger  13872  eqgid  13874  eqgen  13875  qusgrp  13880  qusadd  13882  qusinv  13884  qussub  13885  ghminv  13898  ghmsub  13899  ghmrn  13905  resghm2b  13910  ghmf1  13921  conjsubg  13925  conjsubgen  13926  qusghm  13930  cmncom  13950  ablsubadd  13960  ablsubsub23  13973  ghmcmn  13975  gsumfzreidx  13985  mgpress  14006  srg1expzeq1  14070  ringinvnz1ne0  14124  ringinvnzdiv  14125  dvdsrd  14170  dvdsunit  14188  unitinvcl  14199  unitinvinv  14200  unitlinv  14202  unitrinv  14203  rhmunitinv  14254  subrngintm  14288  subrg1  14307  subrguss  14312  subrginv  14313  subrgunit  14315  subrgugrp  14316  subrgintm  14319  resrhm  14324  resrhm2b  14325  lmodass  14379  lmodlcan  14380  lmod0vlid  14394  lmod0vrid  14395  lmod0vid  14396  lmodvs0  14398  lcomf  14403  lmodvnegcl  14404  lmodvnegid  14405  lmodvsubadd  14414  lmodsubid  14423  lss1d  14459  lspval  14466  lspsnel6  14484  lspsnneg  14496  sralmod  14526  dflidl2rng  14557  lidlacl  14560  dflidl2  14564  df2idl2  14585  qusmul2  14605  quscrng  14609  cnfldmulg  14652  znf1o  14727  znidom  14733  psraddcl  14761  psr0lid  14763  tgss3  14869  clsval  14902  clsss3  14921  neiss2  14933  resttop  14961  resttopon2  14969  lmconst  15007  cnima  15011  cnntri  15015  cncnp  15021  cnrest  15026  cndis  15032  lmss  15037  lmff  15040  lmtopcnp  15041  txcnp  15062  upxp  15063  uptx  15065  cnmpt11  15074  hmeoima  15101  hmeoopn  15102  hmeocld  15103  hmeontr  15104  hmeoimaf1o  15105  mettri2  15153  met0  15155  metres2  15172  blpnf  15191  xblss2ps  15195  xblss2  15196  blbas  15224  blres  15225  xmetec  15228  mopnss  15241  xmstri2  15261  mstri2  15262  xmstri  15263  mstri  15264  xmstri3  15265  mstri3  15266  msrtri  15267  mopni3  15275  unimopn  15277  comet  15290  bdxmet  15292  climcncf  15375  dedekindeulemuub  15408  dedekindicclemuub  15417  ivthdichlem  15442  dvfgg  15479  dvidlemap  15482  dvidrelem  15483  dvidsslem  15484  dvfre  15501  dvmptfsum  15516  plyadd  15542  plymul  15543  reeff1olem  15562  reeff1o  15564  sinperlem  15599  abssinper  15637  reexplog  15662  relogexp  15663  cxpexpnn  15687  cxprec  15701  rpcxpmul2  15704  abscxp  15706  wilthlem1  15774  sgmval2  15778  sgmnncl  15782  0sgmppw  15787  perfectlem1  15793  lgsdir  15834  lgsprme0  15841  lgsdinn0  15847  gausslemma2dlem3  15862  gausslemma2dlem5a  15864  2lgslem1a2  15886  2lgslem1a  15887  2lgslem3  15900  2lgs  15903  umgredgprv  16036  umgrislfupgrdom  16052  uspgredgiedg  16099  uspgriedgedg  16100  usgrislfuspgrdom  16111  usgredg2en  16116  usgredgprv  16117  usgrpredgv  16119  usgredg  16121  usgrnloopv  16122  usgredgne  16125  usgredg3  16135  usgredgedg  16148  usgredgdomord  16151  usgr1vr  16169  subgruhgrfun  16189  subupgr  16194  subumgr  16195  subusgr  16196  umgrwlknloop  16289  wlkres  16300  clwwlkccatlem  16321  clwwlkccat  16322  depindlem1  16427  depindlem2  16428  depindlem3  16429  bj-inex  16603  bj-nn0suc  16660  bj-nn0sucALT  16674  trilpolemeq1  16752  trilpolemlt1  16753  trirec0  16756  nconstwlpolemgt0  16777