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  941  3adantl1  1156  3adantl2  1157  3adantl3  1158  syl3anl1  1298  syl3anl3  1300  syl3anl  1301  stoic3  1451  eupick  2134  csbiebt  3137  csbnestgf  3150  reuss2  3457  mpteq12  4134  otexg  4281  opelopabt  4315  sonr  4371  sotr  4372  issod  4373  so2nr  4375  so3nr  4376  ordelss  4433  onelon  4438  elrnmpt1s  4936  iota2  5269  funeu  5304  imadif  5362  fnbr  5386  feu  5469  f1ss  5498  f1ssres  5501  f1resf1  5502  dffo2  5513  foco  5520  foun  5552  fun11iun  5554  ffoss  5565  funbrfv  5629  fvco3  5662  fvopab6  5688  funfvbrb  5705  elpreima  5711  ffvelcdm  5725  ffvelcdmda  5727  dffo4  5740  fmptco  5758  fsn2  5766  fvconst2g  5810  fex  5825  funfvima  5828  f1elima  5854  f1ocnvfv1  5858  f1ocnvfv2  5859  cocan2  5869  foeqcnvco  5871  isocnv  5892  isores2  5894  isoini  5899  isoselem  5901  f1oiso  5907  f1ofveu  5944  eloprabga  6044  suppssof1  6188  ofco  6189  offveqb  6190  ofc1g  6192  ofc2g  6193  caofid0l  6197  caofid0r  6198  caofid1  6199  caofid2  6200  fnexALT  6208  f1dmex  6213  ot1stg  6250  ot2ndg  6251  ot3rdgg  6252  eqopi  6270  2ndrn  6281  fo2ndf  6325  smores3  6391  smores2  6392  smoel  6398  smoiso  6400  tfrlem1  6406  tfrlemisucaccv  6423  tfrlemibxssdm  6425  tfrlemiubacc  6428  tfr1onlemsucaccv  6439  tfr1onlembfn  6442  tfr1onlemubacc  6444  tfr1onlemaccex  6446  tfr1onlemres  6447  tfrcllemsucaccv  6452  tfrcllembfn  6455  tfrcllemubacc  6457  tfrcllemaccex  6459  tfrcllemres  6460  tfrcl  6462  frecrdg  6506  omv2  6563  nnasuc  6574  nnmsuc  6575  nnacom  6582  nnaass  6583  nnmass  6585  nntri1  6594  nndifsnid  6605  nnmordi  6614  swoer  6660  erth  6678  riinerm  6707  qliftlem  6712  ecovass  6743  ecoviass  6744  elmapssres  6772  fvixp  6802  f1domg  6861  domssr  6881  endomtr  6894  xpsnen2g  6938  enen1  6951  enen2  6952  domen1  6953  domen2  6954  mapen  6957  mapxpen  6959  ssenen  6962  phplem1  6963  fidifsnid  6982  findcard  6999  findcard2  7000  findcard2s  7001  fieq0  7092  isotilem  7122  supisolem  7124  inflbti  7140  ordiso2  7151  djuex  7159  updjudhcoinlf  7196  updjudhcoinrg  7197  updjud  7198  ctssdccl  7227  enumctlemm  7230  nnnninf  7242  finomni  7256  pm54.43  7312  acfun  7334  ccfunen  7391  cc2lem  7393  cc3  7395  addclpi  7455  addasspig  7458  mulasspig  7460  addnidpig  7464  nnppipi  7471  ltanqi  7530  ltmnqi  7531  ltexnqq  7536  archnqq  7545  prarloclemarch2  7547  enq0sym  7560  enq0tr  7562  nqnq0pi  7566  nqnq0  7569  mulcanenq0ec  7573  addclnq0  7579  nqpnq0nq  7581  distrnq0  7587  addassnq0lemcl  7589  addassnq0  7590  prubl  7614  prarloclemlt  7621  genpdf  7636  genipv  7637  genpelvl  7640  genpelvu  7641  genpml  7645  genpmu  7646  genprndl  7649  genprndu  7650  genpassl  7652  genpassu  7653  genpassg  7654  addnqprl  7657  addnqpru  7658  addlocpr  7664  nqprm  7670  nqprl  7679  nqpru  7680  mulnqprl  7696  mulnqpru  7697  mullocprlem  7698  mullocpr  7699  addcomprg  7706  mulcomprg  7708  distrlem1prl  7710  distrlem1pru  7711  distrlem4prl  7712  distrlem4pru  7713  ltprordil  7717  1idprl  7718  1idpru  7719  ltpopr  7723  ltsopr  7724  ltaddpr  7725  ltexprlemm  7728  ltexprlemopl  7729  ltexprlemlol  7730  ltexprlemopu  7731  ltexprlemupu  7732  ltexprlemdisj  7734  ltexprlemloc  7735  ltexprlemfl  7737  ltexprlemrl  7738  ltexprlemfu  7739  ltexprlemru  7740  addcanprleml  7742  addcanprlemu  7743  prplnqu  7748  recexprlemloc  7759  recexprlem1ssl  7761  recexprlem1ssu  7762  recexprlemss1l  7763  recexprlemss1u  7764  aptiprleml  7767  aptiprlemu  7768  cauappcvgprlemloc  7780  cauappcvgprlemladdru  7784  cauappcvgprlemladdrl  7785  caucvgprlemloc  7803  caucvgprlemladdrl  7806  caucvgprprlemml  7822  caucvgprprlemloc  7831  00sr  7897  map2psrprg  7933  suplocsrlempr  7935  suplocsrlem  7936  adddir  8078  axsuploc  8160  eqle  8179  le2tri3i  8196  mul4  8219  muladd11  8220  cnegexlem3  8264  addsub12  8300  2addsub  8301  addsubeq4  8302  subadd4  8331  negcon1  8339  negdi2  8345  negsubdi2  8346  neg2sub  8347  renegcl  8348  muladd  8471  subdir  8473  gt0ne0  8515  ltnegcon1  8551  lenegcon1  8554  eqord1  8571  eqord2  8572  recexre  8666  ltmul1  8680  recexap  8741  div12ap  8782  rerecapb  8931  p1le  8937  ltmul2  8944  gt0div  8958  ge0div  8959  zlem1lt  9444  nnaddm1cl  9449  zdceq  9463  gtndiv  9483  prime  9487  msqznn  9488  btwnz  9507  uzss  9684  eluzadd  9692  nn0pzuz  9723  supinfneg  9731  infsupneg  9732  divfnzn  9757  qnegcl  9772  qreccl  9778  elpqb  9786  xaddass  10006  xleadd1a  10010  xlesubadd  10020  elico2  10074  iccss  10078  iccsupr  10103  elfz5  10154  fznn  10226  difelfznle  10272  fzoaddel  10333  elincfzoext  10339  qdceq  10404  qbtwnxr  10417  flqbi2  10451  adddivflid  10452  fldivnn0  10455  divfl0  10456  flqmulnn0  10459  fldivnn0le  10463  fldiv4p1lem1div2  10465  ceiqle  10475  flqdiv  10483  modqmulnn  10504  frecuzrdgtcl  10574  frecuzrdgsuc  10576  frecuzrdgdomlem  10579  frecuzrdgfunlem  10581  frecuzrdgsuctlem  10585  seqm1g  10636  seq3caopr2  10655  seqcaopr2g  10656  iseqf1olemkle  10659  seq3f1olemp  10677  seqf1oglem2  10682  seqf1og  10683  seq3id  10687  seq3z  10690  expap0  10731  mulexp  10740  mulexpzap  10741  expmul  10746  leexp1a  10756  expubnd  10758  zesq  10820  bernneq  10822  bernneq3  10824  modqexp  10828  facdiv  10900  facndiv  10901  faclbnd3  10905  faclbnd6  10906  bccmpl  10916  bcpasc  10928  bccl  10929  seq3coll  11004  fundm2domnop  11008  wrdsymb1  11047  ccatfv0  11077  ccatrn  11083  ccat2s1cl  11105  lswccats1fst  11114  swrdspsleq  11138  pfxtrcfv  11164  pfxsuffeqwrdeq  11169  pfxlswccat  11184  wrdeqs1cat  11191  cats1un  11192  shftlem  11197  ovshftex  11200  shftval4  11209  shftf  11211  shftcan2  11216  crim  11239  mulreap  11245  remul2  11254  immul2  11261  cjexp  11274  caucvgre  11362  r19.2uz  11374  sqrtsq2  11424  absnid  11454  absexp  11460  nn0abscl  11466  abslt  11469  lenegsq  11476  cau3lem  11495  minmax  11611  xrmaxadd  11642  clim  11662  climshftlemg  11683  climcn1  11689  climcn1lem  11700  clim2ser  11718  clim2ser2  11719  iserex  11720  isermulc2  11721  climub  11725  climcaucn  11732  serf0  11733  summodclem3  11761  summodclem2a  11762  summodclem2  11763  summodc  11764  fsum3  11768  fsumf1o  11771  fisumss  11773  isumss2  11774  fsumcl2lem  11779  fsumadd  11787  fsumsplit  11788  isummulc2  11807  fsum2d  11816  fsummulc2  11829  telfsumo  11847  fsumparts  11851  hash2iun1dif1  11861  bcxmas  11870  isumshft  11871  isumsplit  11872  expcnvap0  11883  geolim  11892  geolim2  11893  cvgratnnlemmn  11906  cvgratnnlemseq  11907  mertenslemi1  11916  mertenslem2  11917  mertensabs  11918  clim2divap  11921  prodmodclem3  11956  prodmodclem2a  11957  fprodseq  11964  fprodf1o  11969  fprodmul  11972  fprodsplitdc  11977  efcllemp  12039  reefcl  12049  efcj  12054  efaddlem  12055  efexp  12063  reeftlcl  12070  eftlub  12071  efsep  12072  effsumlt  12073  eflegeo  12082  retanclap  12103  demoivre  12154  demoivreALT  12155  eirraplem  12158  dvdsval3  12172  p1modz1  12175  iddvdsexp  12196  alzdvds  12235  addmodlteqALT  12240  nnehalf  12285  nno  12287  ndvdsadd  12312  bitsp1e  12333  bitsp1o  12334  bitsinv1  12343  divgcdnnr  12367  neggcd  12374  gcdabs  12379  bezoutlemmain  12389  bezoutlemaz  12394  bezoutlembz  12395  gcdmultiplez  12412  gcdzeq  12413  dvdssq  12422  nninfctlemfo  12431  algrf  12437  algcvg  12440  algcvga  12443  algfx  12444  eucalgf  12447  eucalgcvga  12450  neglcm  12467  lcmabs  12468  lcmdvds  12471  lcmgcdeq  12475  qredeq  12488  isprm3  12510  coprm  12536  prmrp  12537  isprm6  12539  prmdvdsexpb  12541  rpexp  12545  cncongrprm  12549  sqrt2irraplemnn  12571  phibndlem  12608  phiprmpw  12614  eulerthlemh  12623  eulerthlemth  12624  fermltl  12626  prmdivdiv  12629  modprm1div  12640  m1dvdsndvds  12641  coprimeprodsq  12650  pczpre  12690  pczcl  12691  pcexp  12702  pczdvds  12707  pczndvds  12709  pczndvds2  12711  pcdvdsb  12713  pcneg  12718  pcprmpw  12727  difsqpwdvds  12731  pcmptcl  12735  pcprod  12739  fldivp1  12741  infpnlem2  12753  1arithlem4  12759  ennnfonelemrn  12860  topnidg  13154  pwselbasb  13195  pwsplusgval  13197  pwsmulrval  13198  imasaddfnlemg  13216  imasaddflemg  13218  qusin  13228  mgmlrid  13281  mndass  13326  prdsidlem  13349  mhmco  13392  gsumsubm  13396  gsumwcl  13399  gsumwmhm  13400  grpass  13411  grpinvex  13412  dfgrp2  13429  grplid  13433  grprid  13434  grprcan  13439  grpinvssd  13479  grpinvval2  13485  prdsinvlem  13510  pwsinvg  13514  mhmid  13521  mhmmnd  13522  ghmgrp  13524  mulgnn  13532  mulgnnp1  13536  mulgnegnn  13538  mulgnnsubcl  13540  mulgz  13556  issubg2m  13595  issubg4m  13599  subgintm  13604  nmzbi  13615  eqger  13630  eqgid  13632  eqgen  13633  qusgrp  13638  qusadd  13640  qusinv  13642  qussub  13643  ghminv  13656  ghmsub  13657  ghmrn  13663  resghm2b  13668  ghmf1  13679  conjsubg  13683  conjsubgen  13684  qusghm  13688  cmncom  13708  ablsubadd  13718  ablsubsub23  13731  ghmcmn  13733  gsumfzreidx  13743  mgpress  13763  srg1expzeq1  13827  ringinvnz1ne0  13881  ringinvnzdiv  13882  dvdsrd  13926  dvdsunit  13944  unitinvcl  13955  unitinvinv  13956  unitlinv  13958  unitrinv  13959  rhmunitinv  14010  subrngintm  14044  subrg1  14063  subrguss  14068  subrginv  14069  subrgunit  14071  subrgugrp  14072  subrgintm  14075  resrhm  14080  resrhm2b  14081  lmodass  14135  lmodlcan  14136  lmod0vlid  14150  lmod0vrid  14151  lmod0vid  14152  lmodvs0  14154  lcomf  14159  lmodvnegcl  14160  lmodvnegid  14161  lmodvsubadd  14170  lmodsubid  14179  lss1d  14215  lspval  14222  lspsnel6  14240  lspsnneg  14252  sralmod  14282  dflidl2rng  14313  lidlacl  14316  dflidl2  14320  df2idl2  14341  qusmul2  14361  quscrng  14365  cnfldmulg  14408  znf1o  14483  znidom  14489  psraddcl  14512  psr0lid  14514  tgss3  14620  clsval  14653  clsss3  14672  neiss2  14684  resttop  14712  resttopon2  14720  lmconst  14758  cnima  14762  cnntri  14766  cncnp  14772  cnrest  14777  cndis  14783  lmss  14788  lmff  14791  lmtopcnp  14792  txcnp  14813  upxp  14814  uptx  14816  cnmpt11  14825  hmeoima  14852  hmeoopn  14853  hmeocld  14854  hmeontr  14855  hmeoimaf1o  14856  mettri2  14904  met0  14906  metres2  14923  blpnf  14942  xblss2ps  14946  xblss2  14947  blbas  14975  blres  14976  xmetec  14979  mopnss  14992  xmstri2  15012  mstri2  15013  xmstri  15014  mstri  15015  xmstri3  15016  mstri3  15017  msrtri  15018  mopni3  15026  unimopn  15028  comet  15041  bdxmet  15043  climcncf  15126  dedekindeulemuub  15159  dedekindicclemuub  15168  ivthdichlem  15193  dvfgg  15230  dvidlemap  15233  dvidrelem  15234  dvidsslem  15235  dvfre  15252  dvmptfsum  15267  plyadd  15293  plymul  15294  reeff1olem  15313  reeff1o  15315  sinperlem  15350  abssinper  15388  reexplog  15413  relogexp  15414  cxpexpnn  15438  cxprec  15452  rpcxpmul2  15455  abscxp  15457  wilthlem1  15522  sgmval2  15526  sgmnncl  15530  0sgmppw  15535  perfectlem1  15541  lgsdir  15582  lgsprme0  15589  lgsdinn0  15595  gausslemma2dlem3  15610  gausslemma2dlem5a  15612  2lgslem1a2  15634  2lgslem1a  15635  2lgslem3  15648  2lgs  15651  bj-inex  15977  bj-nn0suc  16034  bj-nn0sucALT  16048  trilpolemeq1  16114  trilpolemlt1  16115  trirec0  16118  nconstwlpolemgt0  16138