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  571  pm4.55dc  946  dfifp2dc  989  3adantl1  1179  3adantl2  1180  3adantl3  1181  syl3anl1  1321  syl3anl3  1323  syl3anl  1324  stoic3  1475  eupick  2159  csbiebt  3167  csbnestgf  3180  reuss2  3487  mpteq12  4172  otexg  4322  opelopabt  4356  sonr  4414  sotr  4415  issod  4416  so2nr  4418  so3nr  4419  ordelss  4476  onelon  4481  elrnmpt1s  4982  iota2  5316  funeu  5351  imadif  5410  fnbr  5434  feu  5519  f1ss  5548  f1ssres  5551  f1resf1  5552  dffo2  5563  foco  5570  foun  5602  fun11iun  5604  ffoss  5616  funbrfv  5682  fvco3  5717  fvopab6  5743  funfvbrb  5760  elpreima  5766  ffvelcdm  5780  ffvelcdmda  5782  dffo4  5795  fmptco  5813  fsn2  5821  fncofn  5832  fvconst2g  5868  fex  5883  funfvima  5886  f1elima  5914  f1ocnvfv1  5918  f1ocnvfv2  5919  cocan2  5929  foeqcnvco  5931  isocnv  5952  isores2  5954  isoini  5959  isoselem  5961  f1oiso  5967  f1ofveu  6006  eloprabga  6108  suppssof1  6253  ofco  6254  offveqb  6255  ofc1g  6257  ofc2g  6258  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  fnexALT  6273  f1dmex  6278  ot1stg  6315  ot2ndg  6316  ot3rdgg  6317  eqopi  6335  2ndrn  6346  fo2ndf  6392  smores3  6459  smores2  6460  smoel  6466  smoiso  6468  tfrlem1  6474  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemiubacc  6496  tfr1onlemsucaccv  6507  tfr1onlembfn  6510  tfr1onlemubacc  6512  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembfn  6523  tfrcllemubacc  6525  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  frecrdg  6574  omv2  6633  nnasuc  6644  nnmsuc  6645  nnacom  6652  nnaass  6653  nnmass  6655  nntri1  6664  nndifsnid  6675  nnmordi  6684  swoer  6730  erth  6748  riinerm  6777  qliftlem  6782  ecovass  6813  ecoviass  6814  elmapssres  6842  fvixp  6872  f1domg  6931  domssr  6951  endomtr  6964  xpsnen2g  7013  enen1  7026  enen2  7027  domen1  7028  domen2  7029  mapen  7032  mapxpen  7034  ssenen  7037  phplem1  7038  fidifsnid  7058  findcard  7077  findcard2  7078  findcard2s  7079  fidcen  7088  fieq0  7175  isotilem  7205  supisolem  7207  inflbti  7223  ordiso2  7234  djuex  7242  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  ctssdccl  7310  enumctlemm  7313  nnnninf  7325  finomni  7339  pm54.43  7395  acfun  7422  ccfunen  7483  cc2lem  7485  cc3  7487  addclpi  7547  addasspig  7550  mulasspig  7552  addnidpig  7556  nnppipi  7563  ltanqi  7622  ltmnqi  7623  ltexnqq  7628  archnqq  7637  prarloclemarch2  7639  enq0sym  7652  enq0tr  7654  nqnq0pi  7658  nqnq0  7661  mulcanenq0ec  7665  addclnq0  7671  nqpnq0nq  7673  distrnq0  7679  addassnq0lemcl  7681  addassnq0  7682  prubl  7706  prarloclemlt  7713  genpdf  7728  genipv  7729  genpelvl  7732  genpelvu  7733  genpml  7737  genpmu  7738  genprndl  7741  genprndu  7742  genpassl  7744  genpassu  7745  genpassg  7746  addnqprl  7749  addnqpru  7750  addlocpr  7756  nqprm  7762  nqprl  7771  nqpru  7772  mulnqprl  7788  mulnqpru  7789  mullocprlem  7790  mullocpr  7791  addcomprg  7798  mulcomprg  7800  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  ltprordil  7809  1idprl  7810  1idpru  7811  ltpopr  7815  ltsopr  7816  ltaddpr  7817  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  prplnqu  7840  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  aptiprleml  7859  aptiprlemu  7860  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemloc  7895  caucvgprlemladdrl  7898  caucvgprprlemml  7914  caucvgprprlemloc  7923  00sr  7989  map2psrprg  8025  suplocsrlempr  8027  suplocsrlem  8028  adddir  8170  axsuploc  8252  eqle  8271  le2tri3i  8288  mul4  8311  muladd11  8312  cnegexlem3  8356  addsub12  8392  2addsub  8393  addsubeq4  8394  subadd4  8423  negcon1  8431  negdi2  8437  negsubdi2  8438  neg2sub  8439  renegcl  8440  muladd  8563  subdir  8565  gt0ne0  8607  ltnegcon1  8643  lenegcon1  8646  eqord1  8663  eqord2  8664  recexre  8758  ltmul1  8772  recexap  8833  div12ap  8874  rerecapb  9023  p1le  9029  ltmul2  9036  gt0div  9050  ge0div  9051  zlem1lt  9536  nnaddm1cl  9541  zdceq  9555  gtndiv  9575  prime  9579  msqznn  9580  btwnz  9599  uzss  9777  eluzadd  9785  nn0pzuz  9821  supinfneg  9829  infsupneg  9830  divfnzn  9855  qnegcl  9870  qreccl  9876  elpqb  9884  xaddass  10104  xleadd1a  10108  xlesubadd  10118  elico2  10172  iccss  10176  iccsupr  10201  elfz5  10252  fznn  10324  difelfznle  10370  fzoaddel  10433  elincfzoext  10439  qdceq  10505  qbtwnxr  10518  flqbi2  10552  adddivflid  10553  fldivnn0  10556  divfl0  10557  flqmulnn0  10560  fldivnn0le  10564  fldiv4p1lem1div2  10566  ceiqle  10576  flqdiv  10584  modqmulnn  10605  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgdomlem  10680  frecuzrdgfunlem  10682  frecuzrdgsuctlem  10686  seqm1g  10737  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemkle  10760  seq3f1olemp  10778  seqf1oglem2  10783  seqf1og  10784  seq3id  10788  seq3z  10791  expap0  10832  mulexp  10841  mulexpzap  10842  expmul  10847  leexp1a  10857  expubnd  10859  zesq  10921  bernneq  10923  bernneq3  10925  modqexp  10929  facdiv  11001  facndiv  11002  faclbnd3  11006  faclbnd6  11007  bccmpl  11017  bcpasc  11029  bccl  11030  seq3coll  11107  fundm2domnop  11114  wrdsymb1  11154  ccatfv0  11184  ccatrn  11190  ccat2s1cl  11214  lswccats1fst  11225  swrdspsleq  11252  pfxtrcfv  11278  pfxsuffeqwrdeq  11283  pfxlswccat  11298  wrdeqs1cat  11305  cats1un  11306  swrdccatin1  11310  pfxccatin12lem4  11311  swrdccatin2  11314  pfxccatin12  11318  swrdccat  11320  shftlem  11394  ovshftex  11397  shftval4  11406  shftf  11408  shftcan2  11413  crim  11436  mulreap  11442  remul2  11451  immul2  11458  cjexp  11471  caucvgre  11559  r19.2uz  11571  sqrtsq2  11621  absnid  11651  absexp  11657  nn0abscl  11663  abslt  11666  lenegsq  11673  cau3lem  11692  minmax  11808  xrmaxadd  11839  clim  11859  climshftlemg  11880  climcn1  11886  climcn1lem  11897  clim2ser  11915  clim2ser2  11916  iserex  11917  isermulc2  11918  climub  11922  climcaucn  11929  serf0  11930  summodclem3  11959  summodclem2a  11960  summodclem2  11961  summodc  11962  fsum3  11966  fsumf1o  11969  fisumss  11971  isumss2  11972  fsumcl2lem  11977  fsumadd  11985  fsumsplit  11986  isummulc2  12005  fsum2d  12014  fsummulc2  12027  telfsumo  12045  fsumparts  12049  hash2iun1dif1  12059  bcxmas  12068  isumshft  12069  isumsplit  12070  expcnvap0  12081  geolim  12090  geolim2  12091  cvgratnnlemmn  12104  cvgratnnlemseq  12105  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  clim2divap  12119  prodmodclem3  12154  prodmodclem2a  12155  fprodseq  12162  fprodf1o  12167  fprodmul  12170  fprodsplitdc  12175  efcllemp  12237  reefcl  12247  efcj  12252  efaddlem  12253  efexp  12261  reeftlcl  12268  eftlub  12269  efsep  12270  effsumlt  12271  eflegeo  12280  retanclap  12301  demoivre  12352  demoivreALT  12353  eirraplem  12356  dvdsval3  12370  p1modz1  12373  iddvdsexp  12394  alzdvds  12433  addmodlteqALT  12438  nnehalf  12483  nno  12485  ndvdsadd  12510  bitsp1e  12531  bitsp1o  12532  bitsinv1  12541  divgcdnnr  12565  neggcd  12572  gcdabs  12577  bezoutlemmain  12587  bezoutlemaz  12592  bezoutlembz  12593  gcdmultiplez  12610  gcdzeq  12611  dvdssq  12620  nninfctlemfo  12629  algrf  12635  algcvg  12638  algcvga  12641  algfx  12642  eucalgf  12645  eucalgcvga  12648  neglcm  12665  lcmabs  12666  lcmdvds  12669  lcmgcdeq  12673  qredeq  12686  isprm3  12708  coprm  12734  prmrp  12735  isprm6  12737  prmdvdsexpb  12739  rpexp  12743  cncongrprm  12747  sqrt2irraplemnn  12769  phibndlem  12806  phiprmpw  12812  eulerthlemh  12821  eulerthlemth  12822  fermltl  12824  prmdivdiv  12827  modprm1div  12838  m1dvdsndvds  12839  coprimeprodsq  12848  pczpre  12888  pczcl  12889  pcexp  12900  pczdvds  12905  pczndvds  12907  pczndvds2  12909  pcdvdsb  12911  pcneg  12916  pcprmpw  12925  difsqpwdvds  12929  pcmptcl  12933  pcprod  12937  fldivp1  12939  infpnlem2  12951  1arithlem4  12957  ennnfonelemrn  13058  topnidg  13353  pwselbasb  13394  pwsplusgval  13396  pwsmulrval  13397  imasaddfnlemg  13415  imasaddflemg  13417  qusin  13427  mgmlrid  13480  mndass  13525  prdsidlem  13548  mhmco  13591  gsumsubm  13595  gsumwcl  13598  gsumwmhm  13599  grpass  13610  grpinvex  13611  dfgrp2  13628  grplid  13632  grprid  13633  grprcan  13638  grpinvssd  13678  grpinvval2  13684  prdsinvlem  13709  pwsinvg  13713  mhmid  13720  mhmmnd  13721  ghmgrp  13723  mulgnn  13731  mulgnnp1  13735  mulgnegnn  13737  mulgnnsubcl  13739  mulgz  13755  issubg2m  13794  issubg4m  13798  subgintm  13803  nmzbi  13814  eqger  13829  eqgid  13831  eqgen  13832  qusgrp  13837  qusadd  13839  qusinv  13841  qussub  13842  ghminv  13855  ghmsub  13856  ghmrn  13862  resghm2b  13867  ghmf1  13878  conjsubg  13882  conjsubgen  13883  qusghm  13887  cmncom  13907  ablsubadd  13917  ablsubsub23  13930  ghmcmn  13932  gsumfzreidx  13942  mgpress  13963  srg1expzeq1  14027  ringinvnz1ne0  14081  ringinvnzdiv  14082  dvdsrd  14127  dvdsunit  14145  unitinvcl  14156  unitinvinv  14157  unitlinv  14159  unitrinv  14160  rhmunitinv  14211  subrngintm  14245  subrg1  14264  subrguss  14269  subrginv  14270  subrgunit  14272  subrgugrp  14273  subrgintm  14276  resrhm  14281  resrhm2b  14282  lmodass  14336  lmodlcan  14337  lmod0vlid  14351  lmod0vrid  14352  lmod0vid  14353  lmodvs0  14355  lcomf  14360  lmodvnegcl  14361  lmodvnegid  14362  lmodvsubadd  14371  lmodsubid  14380  lss1d  14416  lspval  14423  lspsnel6  14441  lspsnneg  14453  sralmod  14483  dflidl2rng  14514  lidlacl  14517  dflidl2  14521  df2idl2  14542  qusmul2  14562  quscrng  14566  cnfldmulg  14609  znf1o  14684  znidom  14690  psraddcl  14713  psr0lid  14715  tgss3  14821  clsval  14854  clsss3  14873  neiss2  14885  resttop  14913  resttopon2  14921  lmconst  14959  cnima  14963  cnntri  14967  cncnp  14973  cnrest  14978  cndis  14984  lmss  14989  lmff  14992  lmtopcnp  14993  txcnp  15014  upxp  15015  uptx  15017  cnmpt11  15026  hmeoima  15053  hmeoopn  15054  hmeocld  15055  hmeontr  15056  hmeoimaf1o  15057  mettri2  15105  met0  15107  metres2  15124  blpnf  15143  xblss2ps  15147  xblss2  15148  blbas  15176  blres  15177  xmetec  15180  mopnss  15193  xmstri2  15213  mstri2  15214  xmstri  15215  mstri  15216  xmstri3  15217  mstri3  15218  msrtri  15219  mopni3  15227  unimopn  15229  comet  15242  bdxmet  15244  climcncf  15327  dedekindeulemuub  15360  dedekindicclemuub  15369  ivthdichlem  15394  dvfgg  15431  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvfre  15453  dvmptfsum  15468  plyadd  15494  plymul  15495  reeff1olem  15514  reeff1o  15516  sinperlem  15551  abssinper  15589  reexplog  15614  relogexp  15615  cxpexpnn  15639  cxprec  15653  rpcxpmul2  15656  abscxp  15658  wilthlem1  15723  sgmval2  15727  sgmnncl  15731  0sgmppw  15736  perfectlem1  15742  lgsdir  15783  lgsprme0  15790  lgsdinn0  15796  gausslemma2dlem3  15811  gausslemma2dlem5a  15813  2lgslem1a2  15835  2lgslem1a  15836  2lgslem3  15849  2lgs  15852  umgredgprv  15985  umgrislfupgrdom  16001  uspgredgiedg  16048  uspgriedgedg  16049  usgrislfuspgrdom  16060  usgredg2en  16065  usgredgprv  16066  usgrpredgv  16068  usgredg  16070  usgrnloopv  16071  usgredgne  16074  usgredg3  16084  usgredgedg  16097  usgredgdomord  16100  usgr1vr  16118  subgruhgrfun  16138  subupgr  16143  subumgr  16144  subusgr  16145  umgrwlknloop  16238  wlkres  16249  clwwlkccatlem  16270  clwwlkccat  16271  depindlem1  16376  depindlem2  16377  depindlem3  16378  bj-inex  16553  bj-nn0suc  16610  bj-nn0sucALT  16624  trilpolemeq1  16695  trilpolemlt1  16696  trirec0  16699  nconstwlpolemgt0  16720