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	|- ( ph -> ps )
sylan.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan	|- ( ( ph /\ ch ) -> th )

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ( ph -> ps )
2		sylan.2	. . 3 |- ( ( ps /\ ch ) -> th )
3	2	expcom 116	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	mpan9 281	1 |- ( ( ph /\ ch ) -> th )

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  2133  csbiebt  3133  csbnestgf  3146  reuss2  3453  mpteq12  4128  otexg  4275  opelopabt  4309  sonr  4365  sotr  4366  issod  4367  so2nr  4369  so3nr  4370  ordelss  4427  onelon  4432  elrnmpt1s  4929  iota2  5262  funeu  5297  imadif  5355  fnbr  5379  feu  5460  f1ss  5489  f1ssres  5492  f1resf1  5493  dffo2  5504  foco  5511  foun  5543  fun11iun  5545  ffoss  5556  funbrfv  5619  fvco3  5652  fvopab6  5678  funfvbrb  5695  elpreima  5701  ffvelcdm  5715  ffvelcdmda  5717  dffo4  5730  fmptco  5748  fsn2  5756  fvconst2g  5800  fex  5815  funfvima  5818  f1elima  5844  f1ocnvfv1  5848  f1ocnvfv2  5849  cocan2  5859  foeqcnvco  5861  isocnv  5882  isores2  5884  isoini  5889  isoselem  5891  f1oiso  5897  f1ofveu  5934  eloprabga  6034  suppssof1  6178  ofco  6179  offveqb  6180  ofc1g  6182  ofc2g  6183  caofid0l  6187  caofid0r  6188  caofid1  6189  caofid2  6190  fnexALT  6198  f1dmex  6203  ot1stg  6240  ot2ndg  6241  ot3rdgg  6242  eqopi  6260  2ndrn  6271  fo2ndf  6315  smores3  6381  smores2  6382  smoel  6388  smoiso  6390  tfrlem1  6396  tfrlemisucaccv  6413  tfrlemibxssdm  6415  tfrlemiubacc  6418  tfr1onlemsucaccv  6429  tfr1onlembfn  6432  tfr1onlemubacc  6434  tfr1onlemaccex  6436  tfr1onlemres  6437  tfrcllemsucaccv  6442  tfrcllembfn  6445  tfrcllemubacc  6447  tfrcllemaccex  6449  tfrcllemres  6450  tfrcl  6452  frecrdg  6496  omv2  6553  nnasuc  6564  nnmsuc  6565  nnacom  6572  nnaass  6573  nnmass  6575  nntri1  6584  nndifsnid  6595  nnmordi  6604  swoer  6650  erth  6668  riinerm  6697  qliftlem  6702  ecovass  6733  ecoviass  6734  elmapssres  6762  fvixp  6792  f1domg  6851  domssr  6871  endomtr  6884  xpsnen2g  6926  enen1  6939  enen2  6940  domen1  6941  domen2  6942  mapen  6945  mapxpen  6947  ssenen  6950  phplem1  6951  fidifsnid  6970  findcard  6987  findcard2  6988  findcard2s  6989  fieq0  7080  isotilem  7110  supisolem  7112  inflbti  7128  ordiso2  7139  djuex  7147  updjudhcoinlf  7184  updjudhcoinrg  7185  updjud  7186  ctssdccl  7215  enumctlemm  7218  nnnninf  7230  finomni  7244  pm54.43  7300  acfun  7321  ccfunen  7378  cc2lem  7380  cc3  7382  addclpi  7442  addasspig  7445  mulasspig  7447  addnidpig  7451  nnppipi  7458  ltanqi  7517  ltmnqi  7518  ltexnqq  7523  archnqq  7532  prarloclemarch2  7534  enq0sym  7547  enq0tr  7549  nqnq0pi  7553  nqnq0  7556  mulcanenq0ec  7560  addclnq0  7566  nqpnq0nq  7568  distrnq0  7574  addassnq0lemcl  7576  addassnq0  7577  prubl  7601  prarloclemlt  7608  genpdf  7623  genipv  7624  genpelvl  7627  genpelvu  7628  genpml  7632  genpmu  7633  genprndl  7636  genprndu  7637  genpassl  7639  genpassu  7640  genpassg  7641  addnqprl  7644  addnqpru  7645  addlocpr  7651  nqprm  7657  nqprl  7666  nqpru  7667  mulnqprl  7683  mulnqpru  7684  mullocprlem  7685  mullocpr  7686  addcomprg  7693  mulcomprg  7695  distrlem1prl  7697  distrlem1pru  7698  distrlem4prl  7699  distrlem4pru  7700  ltprordil  7704  1idprl  7705  1idpru  7706  ltpopr  7710  ltsopr  7711  ltaddpr  7712  ltexprlemm  7715  ltexprlemopl  7716  ltexprlemlol  7717  ltexprlemopu  7718  ltexprlemupu  7719  ltexprlemdisj  7721  ltexprlemloc  7722  ltexprlemfl  7724  ltexprlemrl  7725  ltexprlemfu  7726  ltexprlemru  7727  addcanprleml  7729  addcanprlemu  7730  prplnqu  7735  recexprlemloc  7746  recexprlem1ssl  7748  recexprlem1ssu  7749  recexprlemss1l  7750  recexprlemss1u  7751  aptiprleml  7754  aptiprlemu  7755  cauappcvgprlemloc  7767  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  caucvgprlemloc  7790  caucvgprlemladdrl  7793  caucvgprprlemml  7809  caucvgprprlemloc  7818  00sr  7884  map2psrprg  7920  suplocsrlempr  7922  suplocsrlem  7923  adddir  8065  axsuploc  8147  eqle  8166  le2tri3i  8183  mul4  8206  muladd11  8207  cnegexlem3  8251  addsub12  8287  2addsub  8288  addsubeq4  8289  subadd4  8318  negcon1  8326  negdi2  8332  negsubdi2  8333  neg2sub  8334  renegcl  8335  muladd  8458  subdir  8460  gt0ne0  8502  ltnegcon1  8538  lenegcon1  8541  eqord1  8558  eqord2  8559  recexre  8653  ltmul1  8667  recexap  8728  div12ap  8769  rerecapb  8918  p1le  8924  ltmul2  8931  gt0div  8945  ge0div  8946  zlem1lt  9431  nnaddm1cl  9436  zdceq  9450  gtndiv  9470  prime  9474  msqznn  9475  btwnz  9494  uzss  9671  eluzadd  9679  nn0pzuz  9710  supinfneg  9718  infsupneg  9719  divfnzn  9744  qnegcl  9759  qreccl  9765  elpqb  9773  xaddass  9993  xleadd1a  9997  xlesubadd  10007  elico2  10061  iccss  10065  iccsupr  10090  elfz5  10141  fznn  10213  difelfznle  10259  fzoaddel  10318  elincfzoext  10324  qdceq  10389  qbtwnxr  10402  flqbi2  10436  adddivflid  10437  fldivnn0  10440  divfl0  10441  flqmulnn0  10444  fldivnn0le  10448  fldiv4p1lem1div2  10450  ceiqle  10460  flqdiv  10468  modqmulnn  10489  frecuzrdgtcl  10559  frecuzrdgsuc  10561  frecuzrdgdomlem  10564  frecuzrdgfunlem  10566  frecuzrdgsuctlem  10570  seqm1g  10621  seq3caopr2  10640  seqcaopr2g  10641  iseqf1olemkle  10644  seq3f1olemp  10662  seqf1oglem2  10667  seqf1og  10668  seq3id  10672  seq3z  10675  expap0  10716  mulexp  10725  mulexpzap  10726  expmul  10731  leexp1a  10741  expubnd  10743  zesq  10805  bernneq  10807  bernneq3  10809  modqexp  10813  facdiv  10885  facndiv  10886  faclbnd3  10890  faclbnd6  10891  bccmpl  10901  bcpasc  10913  bccl  10914  seq3coll  10989  fundm2domnop  10993  wrdsymb1  11032  ccatfv0  11062  ccatrn  11068  ccat2s1cl  11090  lswccats1fst  11099  swrdspsleq  11123  pfxtrcfv  11147  pfxsuffeqwrdeq  11152  shftlem  11160  ovshftex  11163  shftval4  11172  shftf  11174  shftcan2  11179  crim  11202  mulreap  11208  remul2  11217  immul2  11224  cjexp  11237  caucvgre  11325  r19.2uz  11337  sqrtsq2  11387  absnid  11417  absexp  11423  nn0abscl  11429  abslt  11432  lenegsq  11439  cau3lem  11458  minmax  11574  xrmaxadd  11605  clim  11625  climshftlemg  11646  climcn1  11652  climcn1lem  11663  clim2ser  11681  clim2ser2  11682  iserex  11683  isermulc2  11684  climub  11688  climcaucn  11695  serf0  11696  summodclem3  11724  summodclem2a  11725  summodclem2  11726  summodc  11727  fsum3  11731  fsumf1o  11734  fisumss  11736  isumss2  11737  fsumcl2lem  11742  fsumadd  11750  fsumsplit  11751  isummulc2  11770  fsum2d  11779  fsummulc2  11792  telfsumo  11810  fsumparts  11814  hash2iun1dif1  11824  bcxmas  11833  isumshft  11834  isumsplit  11835  expcnvap0  11846  geolim  11855  geolim2  11856  cvgratnnlemmn  11869  cvgratnnlemseq  11870  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  clim2divap  11884  prodmodclem3  11919  prodmodclem2a  11920  fprodseq  11927  fprodf1o  11932  fprodmul  11935  fprodsplitdc  11940  efcllemp  12002  reefcl  12012  efcj  12017  efaddlem  12018  efexp  12026  reeftlcl  12033  eftlub  12034  efsep  12035  effsumlt  12036  eflegeo  12045  retanclap  12066  demoivre  12117  demoivreALT  12118  eirraplem  12121  dvdsval3  12135  p1modz1  12138  iddvdsexp  12159  alzdvds  12198  addmodlteqALT  12203  nnehalf  12248  nno  12250  ndvdsadd  12275  bitsp1e  12296  bitsp1o  12297  bitsinv1  12306  divgcdnnr  12330  neggcd  12337  gcdabs  12342  bezoutlemmain  12352  bezoutlemaz  12357  bezoutlembz  12358  gcdmultiplez  12375  gcdzeq  12376  dvdssq  12385  nninfctlemfo  12394  algrf  12400  algcvg  12403  algcvga  12406  algfx  12407  eucalgf  12410  eucalgcvga  12413  neglcm  12430  lcmabs  12431  lcmdvds  12434  lcmgcdeq  12438  qredeq  12451  isprm3  12473  coprm  12499  prmrp  12500  isprm6  12502  prmdvdsexpb  12504  rpexp  12508  cncongrprm  12512  sqrt2irraplemnn  12534  phibndlem  12571  phiprmpw  12577  eulerthlemh  12586  eulerthlemth  12587  fermltl  12589  prmdivdiv  12592  modprm1div  12603  m1dvdsndvds  12604  coprimeprodsq  12613  pczpre  12653  pczcl  12654  pcexp  12665  pczdvds  12670  pczndvds  12672  pczndvds2  12674  pcdvdsb  12676  pcneg  12681  pcprmpw  12690  difsqpwdvds  12694  pcmptcl  12698  pcprod  12702  fldivp1  12704  infpnlem2  12716  1arithlem4  12722  ennnfonelemrn  12823  topnidg  13117  pwselbasb  13158  pwsplusgval  13160  pwsmulrval  13161  imasaddfnlemg  13179  imasaddflemg  13181  qusin  13191  mgmlrid  13244  mndass  13289  prdsidlem  13312  mhmco  13355  gsumsubm  13359  gsumwcl  13362  gsumwmhm  13363  grpass  13374  grpinvex  13375  dfgrp2  13392  grplid  13396  grprid  13397  grprcan  13402  grpinvssd  13442  grpinvval2  13448  prdsinvlem  13473  pwsinvg  13477  mhmid  13484  mhmmnd  13485  ghmgrp  13487  mulgnn  13495  mulgnnp1  13499  mulgnegnn  13501  mulgnnsubcl  13503  mulgz  13519  issubg2m  13558  issubg4m  13562  subgintm  13567  nmzbi  13578  eqger  13593  eqgid  13595  eqgen  13596  qusgrp  13601  qusadd  13603  qusinv  13605  qussub  13606  ghminv  13619  ghmsub  13620  ghmrn  13626  resghm2b  13631  ghmf1  13642  conjsubg  13646  conjsubgen  13647  qusghm  13651  cmncom  13671  ablsubadd  13681  ablsubsub23  13694  ghmcmn  13696  gsumfzreidx  13706  mgpress  13726  srg1expzeq1  13790  ringinvnz1ne0  13844  ringinvnzdiv  13845  dvdsrd  13889  dvdsunit  13907  unitinvcl  13918  unitinvinv  13919  unitlinv  13921  unitrinv  13922  rhmunitinv  13973  subrngintm  14007  subrg1  14026  subrguss  14031  subrginv  14032  subrgunit  14034  subrgugrp  14035  subrgintm  14038  resrhm  14043  resrhm2b  14044  lmodass  14098  lmodlcan  14099  lmod0vlid  14113  lmod0vrid  14114  lmod0vid  14115  lmodvs0  14117  lcomf  14122  lmodvnegcl  14123  lmodvnegid  14124  lmodvsubadd  14133  lmodsubid  14142  lss1d  14178  lspval  14185  lspsnel6  14203  lspsnneg  14215  sralmod  14245  dflidl2rng  14276  lidlacl  14279  dflidl2  14283  df2idl2  14304  qusmul2  14324  quscrng  14328  cnfldmulg  14371  znf1o  14446  znidom  14452  psraddcl  14475  psr0lid  14477  tgss3  14583  clsval  14616  clsss3  14635  neiss2  14647  resttop  14675  resttopon2  14683  lmconst  14721  cnima  14725  cnntri  14729  cncnp  14735  cnrest  14740  cndis  14746  lmss  14751  lmff  14754  lmtopcnp  14755  txcnp  14776  upxp  14777  uptx  14779  cnmpt11  14788  hmeoima  14815  hmeoopn  14816  hmeocld  14817  hmeontr  14818  hmeoimaf1o  14819  mettri2  14867  met0  14869  metres2  14886  blpnf  14905  xblss2ps  14909  xblss2  14910  blbas  14938  blres  14939  xmetec  14942  mopnss  14955  xmstri2  14975  mstri2  14976  xmstri  14977  mstri  14978  xmstri3  14979  mstri3  14980  msrtri  14981  mopni3  14989  unimopn  14991  comet  15004  bdxmet  15006  climcncf  15089  dedekindeulemuub  15122  dedekindicclemuub  15131  ivthdichlem  15156  dvfgg  15193  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvfre  15215  dvmptfsum  15230  plyadd  15256  plymul  15257  reeff1olem  15276  reeff1o  15278  sinperlem  15313  abssinper  15351  reexplog  15376  relogexp  15377  cxpexpnn  15401  cxprec  15415  rpcxpmul2  15418  abscxp  15420  wilthlem1  15485  sgmval2  15489  sgmnncl  15493  0sgmppw  15498  perfectlem1  15504  lgsdir  15545  lgsprme0  15552  lgsdinn0  15558  gausslemma2dlem3  15573  gausslemma2dlem5a  15575  2lgslem1a2  15597  2lgslem1a  15598  2lgslem3  15611  2lgs  15614  bj-inex  15880  bj-nn0suc  15937  bj-nn0sucALT  15951  trilpolemeq1  16016  trilpolemlt1  16017  trirec0  16020  nconstwlpolemgt0  16040