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  947  dfifp2dc  990  3adantl1  1180  3adantl2  1181  3adantl3  1182  syl3anl1  1322  syl3anl3  1324  syl3anl  1325  stoic3  1476  eupick  2162  csbiebt  3181  csbnestgf  3194  reuss2  3505  mpteq12  4198  otexg  4351  opelopabt  4385  sonr  4443  sotr  4444  issod  4445  so2nr  4447  so3nr  4448  ordelss  4505  onelon  4510  elrnmpt1s  5012  iota2  5347  funeu  5382  imadif  5441  fnbr  5465  feu  5554  f1ss  5584  f1ssres  5587  f1resf1  5588  dffo2  5599  foco  5606  foun  5638  fun11iun  5640  ffoss  5652  funbrfv  5718  fvco3  5753  fvopab6  5779  funfvbrb  5796  elpreima  5802  ffvelcdm  5815  ffvelcdmda  5817  dffo4  5830  fmptco  5848  fsn2  5856  fncofn  5867  fvconst2g  5903  fex  5920  funfvima  5923  f1elima  5952  f1ocnvfv1  5956  f1ocnvfv2  5957  cocan2  5967  foeqcnvco  5969  isocnv  5990  isores2  5992  isoini  5997  isoselem  5999  f1oiso  6005  f1ofveu  6046  eloprabga  6148  suppssof1  6293  ofco  6294  offveqb  6295  ofc1g  6297  ofc2g  6298  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  fnexALT  6313  f1dmex  6318  ot1stg  6359  ot2ndg  6360  ot3rdgg  6361  eqopi  6379  2ndrn  6390  fo2ndf  6436  suppval1  6452  ressuppss  6467  suppssrst  6474  suppssrgst  6475  smores3  6537  smores2  6538  smoel  6544  smoiso  6546  tfrlem1  6552  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemiubacc  6574  tfr1onlemsucaccv  6585  tfr1onlembfn  6588  tfr1onlemubacc  6590  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllembfn  6601  tfrcllemubacc  6603  tfrcllemaccex  6605  tfrcllemres  6606  tfrcl  6608  frecrdg  6652  omv2  6711  nnasuc  6722  nnmsuc  6723  nnacom  6730  nnaass  6731  nnmass  6733  nntri1  6742  nndifsnid  6753  nnmordi  6762  swoer  6808  erth  6826  riinerm  6855  qliftlem  6860  ecovass  6891  ecoviass  6892  elmapssres  6920  fvixp  6951  f1domg  7010  domssr  7030  endomtr  7043  xpsnen2g  7093  enen1  7106  enen2  7107  domen1  7108  domen2  7109  mapen  7112  mapxpen  7114  ssenen  7118  phplem1  7119  fidifsnid  7139  findcard  7158  findcard2  7159  findcard2s  7160  fidcen  7169  fieq0  7276  isotilem  7310  supisolem  7312  inflbti  7328  ordiso2  7339  djuex  7347  updjudhcoinlf  7384  updjudhcoinrg  7385  updjud  7386  ctssdccl  7415  enumctlemm  7418  nnnninf  7430  finomni  7444  pm54.43  7500  acfun  7527  ccfunen  7594  cc2lem  7596  cc3  7598  addclpi  7658  addasspig  7661  mulasspig  7663  addnidpig  7667  nnppipi  7674  ltanqi  7733  ltmnqi  7734  ltexnqq  7739  archnqq  7748  prarloclemarch2  7750  enq0sym  7763  enq0tr  7765  nqnq0pi  7769  nqnq0  7772  mulcanenq0ec  7776  addclnq0  7782  nqpnq0nq  7784  distrnq0  7790  addassnq0lemcl  7792  addassnq0  7793  prubl  7817  prarloclemlt  7824  genpdf  7839  genipv  7840  genpelvl  7843  genpelvu  7844  genpml  7848  genpmu  7849  genprndl  7852  genprndu  7853  genpassl  7855  genpassu  7856  genpassg  7857  addnqprl  7860  addnqpru  7861  addlocpr  7867  nqprm  7873  nqprl  7882  nqpru  7883  mulnqprl  7899  mulnqpru  7900  mullocprlem  7901  mullocpr  7902  addcomprg  7909  mulcomprg  7911  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  ltprordil  7920  1idprl  7921  1idpru  7922  ltpopr  7926  ltsopr  7927  ltaddpr  7928  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  prplnqu  7951  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  aptiprleml  7970  aptiprlemu  7971  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemloc  8006  caucvgprlemladdrl  8009  caucvgprprlemml  8025  caucvgprprlemloc  8034  00sr  8100  map2psrprg  8136  suplocsrlempr  8138  suplocsrlem  8139  adddir  8281  axsuploc  8362  eqle  8381  le2tri3i  8398  mul4  8421  muladd11  8422  cnegexlem3  8466  addsub12  8502  2addsub  8503  addsubeq4  8504  subadd4  8533  negcon1  8541  negdi2  8547  negsubdi2  8548  neg2sub  8549  renegcl  8550  muladd  8674  subdir  8676  gt0ne0  8718  ltnegcon1  8754  lenegcon1  8757  eqord1  8774  eqord2  8775  recexre  8869  ltmul1  8883  recexap  8944  div12ap  8985  rerecapb  9134  p1le  9140  ltmul2  9147  gt0div  9161  ge0div  9162  zlem1lt  9651  nnaddm1cl  9656  zdceq  9670  gtndiv  9691  prime  9695  msqznn  9696  btwnz  9715  uzss  9893  eluzadd  9901  nn0pzuz  9937  supinfneg  9945  infsupneg  9946  divfnzn  9971  qnegcl  9986  qreccl  9992  elpqb  10000  xaddass  10221  xleadd1a  10225  xlesubadd  10235  elico2  10289  iccss  10293  iccsupr  10318  elfz5  10370  fznn  10445  difelfznle  10491  fzoaddel  10554  elincfzoext  10560  qdceq  10628  qbtwnxr  10641  flqbi2  10675  adddivflid  10676  fldivnn0  10679  divfl0  10680  flqmulnn0  10683  fldivnn0le  10687  fldiv4p1lem1div2  10689  ceiqle  10699  flqdiv  10707  modqmulnn  10728  frecuzrdgtcl  10798  frecuzrdgsuc  10800  frecuzrdgdomlem  10803  frecuzrdgfunlem  10805  frecuzrdgsuctlem  10809  seqm1g  10860  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemkle  10883  seq3f1olemp  10901  seqf1oglem2  10906  seqf1og  10907  seq3id  10911  seq3z  10914  expap0  10955  mulexp  10964  mulexpzap  10965  expmul  10970  leexp1a  10980  expubnd  10982  zesq  11045  bernneq  11047  bernneq3  11049  modqexp  11053  facdiv  11125  facndiv  11126  faclbnd3  11130  faclbnd6  11131  bccmpl  11141  bcpasc  11153  bccl  11154  hashfibclem  11231  hashfibc  11232  seq3coll  11239  fundm2domnop  11246  wrdsymb1  11286  ccatfv0  11316  ccatrn  11322  ccat2s1cl  11346  lswccats1fst  11357  swrdspsleq  11384  pfxtrcfv  11410  pfxsuffeqwrdeq  11415  pfxlswccat  11430  wrdeqs1cat  11437  cats1un  11438  swrdccatin1  11442  pfxccatin12lem4  11443  swrdccatin2  11446  pfxccatin12  11450  swrdccat  11452  shftlem  11526  ovshftex  11529  shftval4  11538  shftf  11540  shftcan2  11545  crim  11568  mulreap  11574  remul2  11583  immul2  11590  cjexp  11603  caucvgre  11691  r19.2uz  11703  sqrtsq2  11753  absnid  11783  absexp  11789  nn0abscl  11795  abslt  11798  lenegsq  11805  cau3lem  11824  minmax  11940  xrmaxadd  11971  clim  11991  climshftlemg  12012  climcn1  12018  climcn1lem  12029  clim2ser  12047  clim2ser2  12048  iserex  12049  isermulc2  12050  climub  12054  climcaucn  12061  serf0  12062  summodclem3  12091  summodclem2a  12092  summodclem2  12093  summodc  12094  fsum3  12098  fsumf1o  12101  fisumss  12103  isumss2  12104  fsumcl2lem  12109  fsumadd  12117  fsumsplit  12118  isummulc2  12137  fsum2d  12146  fsummulc2  12159  telfsumo  12177  fsumparts  12181  hash2iun1dif1  12191  bcxmas  12200  isumshft  12201  isumsplit  12202  expcnvap0  12213  geolim  12222  geolim2  12223  cvgratnnlemmn  12236  cvgratnnlemseq  12237  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  clim2divap  12251  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  fprodf1o  12299  fprodmul  12302  fprodsplitdc  12307  efcllemp  12369  reefcl  12379  efcj  12384  efaddlem  12385  efexp  12393  reeftlcl  12400  eftlub  12401  efsep  12402  effsumlt  12403  eflegeo  12412  retanclap  12433  demoivre  12484  demoivreALT  12485  eirraplem  12488  dvdsval3  12502  p1modz1  12505  iddvdsexp  12526  alzdvds  12565  addmodlteqALT  12570  nnehalf  12615  nno  12617  ndvdsadd  12642  bitsp1e  12663  bitsp1o  12664  bitsinv1  12673  divgcdnnr  12697  neggcd  12704  gcdabs  12709  bezoutlemmain  12719  bezoutlemaz  12724  bezoutlembz  12725  gcdmultiplez  12742  gcdzeq  12743  dvdssq  12752  nninfctlemfo  12761  algrf  12767  algcvg  12770  algcvga  12773  algfx  12774  eucalgf  12777  eucalgcvga  12780  neglcm  12797  lcmabs  12798  lcmdvds  12801  lcmgcdeq  12805  qredeq  12818  isprm3  12840  coprm  12866  prmrp  12867  isprm6  12869  prmdvdsexpb  12871  rpexp  12875  cncongrprm  12879  sqrt2irraplemnn  12901  phibndlem  12938  phiprmpw  12944  eulerthlemh  12953  eulerthlemth  12954  fermltl  12956  prmdivdiv  12959  modprm1div  12970  m1dvdsndvds  12971  coprimeprodsq  12980  pczpre  13020  pczcl  13021  pcexp  13032  pczdvds  13037  pczndvds  13039  pczndvds2  13041  pcdvdsb  13043  pcneg  13048  pcprmpw  13057  difsqpwdvds  13061  pcmptcl  13065  pcprod  13069  fldivp1  13071  infpnlem2  13083  1arithlem4  13089  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfrcn0  13217  ennnfonelemrn  13254  topnidg  13549  imasaddfnlemg  13578  imasaddflemg  13580  qusin  13590  mgmlrid  13642  mndass  13685  mhmco  13745  gsumsubm  13749  gsumwcl  13752  gsumwmhm  13753  grpass  13764  grpinvex  13765  dfgrp2  13782  grplid  13786  grprid  13787  grprcan  13792  grpinvssd  13832  grpinvval2  13838  mhmid  13868  mhmmnd  13869  ghmgrp  13871  mulgnn  13879  mulgnnp1  13883  mulgnegnn  13885  mulgnnsubcl  13887  mulgz  13903  issubg2m  13942  issubg4m  13946  subgintm  13951  nmzbi  13962  eqger  13977  eqgid  13979  eqgen  13980  qusgrp  13985  qusadd  13987  qusinv  13989  qussub  13990  ghminv  14003  ghmsub  14004  ghmrn  14010  resghm2b  14015  ghmf1  14026  conjsubg  14030  conjsubgen  14031  qusghm  14035  cmncom  14055  ablsubadd  14065  ablsubsub23  14078  ghmcmn  14080  gsumfzreidx  14090  prdsidlem  14135  prdsinvlem  14138  pwselbasb  14148  pwsplusgval  14150  pwsmulrval  14151  pwsinvg  14157  mgpress  14170  srg1expzeq1  14238  ringinvnz1ne0  14292  ringinvnzdiv  14293  dvdsrd  14339  dvdsunit  14357  unitinvcl  14368  unitinvinv  14369  unitlinv  14371  unitrinv  14372  rhmunitinv  14423  subrngintm  14458  subrg1  14477  subrguss  14482  subrginv  14483  subrgunit  14485  subrgugrp  14486  subrgintm  14489  resrhm  14494  resrhm2b  14495  lmodass  14577  lmodlcan  14578  lmod0vlid  14592  lmod0vrid  14593  lmod0vid  14594  lmodvs0  14596  lcomf  14601  lmodvnegcl  14602  lmodvnegid  14603  lmodvsubadd  14612  lmodsubid  14621  lss1d  14657  lspval  14664  lspsnel6  14682  lspsnneg  14694  sralmod  14724  dflidl2rng  14755  lidlacl  14758  dflidl2  14762  df2idl2  14783  qusmul2  14803  quscrng  14807  cnfldmulg  14850  znf1o  14925  znidom  14931  psraddcl  14961  psr0lid  14963  tgss3  15069  clsval  15102  clsss3  15121  neiss2  15133  resttop  15161  resttopon2  15169  lmconst  15207  cnima  15211  cnntri  15215  cncnp  15221  cnrest  15226  cndis  15232  lmss  15237  lmff  15240  lmtopcnp  15241  txcnp  15262  upxp  15263  uptx  15265  cnmpt11  15274  hmeoima  15301  hmeoopn  15302  hmeocld  15303  hmeontr  15304  hmeoimaf1o  15305  mettri2  15353  met0  15355  metres2  15372  blpnf  15391  xblss2ps  15395  xblss2  15396  blbas  15424  blres  15425  xmetec  15428  mopnss  15441  xmstri2  15461  mstri2  15462  xmstri  15463  mstri  15464  xmstri3  15465  mstri3  15466  msrtri  15467  mopni3  15475  unimopn  15477  comet  15490  bdxmet  15492  climcncf  15575  dedekindeulemuub  15608  dedekindicclemuub  15617  ivthdichlem  15642  dvfgg  15679  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvfre  15701  dvmptfsum  15716  plyadd  15742  plymul  15743  reeff1olem  15762  reeff1o  15764  sinperlem  15799  abssinper  15837  reexplog  15862  relogexp  15863  cxpexpnn  15887  cxprec  15901  rpcxpmul2  15904  abscxp  15906  wilthlem1  15974  sgmval2  15978  sgmnncl  15982  0sgmppw  15987  perfectlem1  15993  lgsdir  16034  lgsprme0  16041  lgsdinn0  16047  gausslemma2dlem3  16062  gausslemma2dlem5a  16064  2lgslem1a2  16086  2lgslem1a  16087  2lgslem3  16100  2lgs  16103  umgredgprv  16236  umgrislfupgrdom  16252  uspgredgiedg  16299  uspgriedgedg  16300  usgrislfuspgrdom  16311  usgredg2en  16316  usgredgprv  16317  usgrpredgv  16319  usgredg  16321  usgrnloopv  16322  usgredgne  16325  usgredg3  16335  usgredgedg  16348  usgredgdomord  16351  usgr1vr  16369  subgruhgrfun  16389  subupgr  16394  subumgr  16395  subusgr  16396  umgrwlknloop  16489  wlkres  16500  clwwlkccatlem  16521  clwwlkccat  16522  depindlem1  16627  depindlem2  16628  depindlem3  16629  bj-inex  16803  bj-nn0suc  16860  bj-nn0sucALT  16874  trilpolemeq1  16950  trilpolemlt1  16951  trirec0  16954  nconstwlpolemgt0  16976