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  3180  csbnestgf  3193  reuss2  3503  mpteq12  4195  otexg  4348  opelopabt  4382  sonr  4440  sotr  4441  issod  4442  so2nr  4444  so3nr  4445  ordelss  4502  onelon  4507  elrnmpt1s  5009  iota2  5344  funeu  5379  imadif  5438  fnbr  5462  feu  5551  f1ss  5581  f1ssres  5584  f1resf1  5585  dffo2  5596  foco  5603  foun  5635  fun11iun  5637  ffoss  5649  funbrfv  5715  fvco3  5750  fvopab6  5776  funfvbrb  5793  elpreima  5799  ffvelcdm  5812  ffvelcdmda  5814  dffo4  5827  fmptco  5845  fsn2  5853  fncofn  5864  fvconst2g  5900  fex  5917  funfvima  5920  f1elima  5948  f1ocnvfv1  5952  f1ocnvfv2  5953  cocan2  5963  foeqcnvco  5965  isocnv  5986  isores2  5988  isoini  5993  isoselem  5995  f1oiso  6001  f1ofveu  6040  eloprabga  6142  suppssof1  6286  ofco  6287  offveqb  6288  ofc1g  6290  ofc2g  6291  caofid0l  6295  caofid0r  6296  caofid1  6297  caofid2  6298  fnexALT  6306  f1dmex  6311  ot1stg  6348  ot2ndg  6349  ot3rdgg  6350  eqopi  6368  2ndrn  6379  fo2ndf  6425  suppval1  6441  ressuppss  6456  suppssrst  6463  suppssrgst  6464  smores3  6526  smores2  6527  smoel  6533  smoiso  6535  tfrlem1  6541  tfrlemisucaccv  6558  tfrlemibxssdm  6560  tfrlemiubacc  6563  tfr1onlemsucaccv  6574  tfr1onlembfn  6577  tfr1onlemubacc  6579  tfr1onlemaccex  6581  tfr1onlemres  6582  tfrcllemsucaccv  6587  tfrcllembfn  6590  tfrcllemubacc  6592  tfrcllemaccex  6594  tfrcllemres  6595  tfrcl  6597  frecrdg  6641  omv2  6700  nnasuc  6711  nnmsuc  6712  nnacom  6719  nnaass  6720  nnmass  6722  nntri1  6731  nndifsnid  6742  nnmordi  6751  swoer  6797  erth  6815  riinerm  6844  qliftlem  6849  ecovass  6880  ecoviass  6881  elmapssres  6909  fvixp  6940  f1domg  6999  domssr  7019  endomtr  7032  xpsnen2g  7082  enen1  7095  enen2  7096  domen1  7097  domen2  7098  mapen  7101  mapxpen  7103  ssenen  7107  phplem1  7108  fidifsnid  7128  findcard  7147  findcard2  7148  findcard2s  7149  fidcen  7158  fieq0  7265  isotilem  7299  supisolem  7301  inflbti  7317  ordiso2  7328  djuex  7336  updjudhcoinlf  7373  updjudhcoinrg  7374  updjud  7375  ctssdccl  7404  enumctlemm  7407  nnnninf  7419  finomni  7433  pm54.43  7489  acfun  7516  ccfunen  7580  cc2lem  7582  cc3  7584  addclpi  7644  addasspig  7647  mulasspig  7649  addnidpig  7653  nnppipi  7660  ltanqi  7719  ltmnqi  7720  ltexnqq  7725  archnqq  7734  prarloclemarch2  7736  enq0sym  7749  enq0tr  7751  nqnq0pi  7755  nqnq0  7758  mulcanenq0ec  7762  addclnq0  7768  nqpnq0nq  7770  distrnq0  7776  addassnq0lemcl  7778  addassnq0  7779  prubl  7803  prarloclemlt  7810  genpdf  7825  genipv  7826  genpelvl  7829  genpelvu  7830  genpml  7834  genpmu  7835  genprndl  7838  genprndu  7839  genpassl  7841  genpassu  7842  genpassg  7843  addnqprl  7846  addnqpru  7847  addlocpr  7853  nqprm  7859  nqprl  7868  nqpru  7869  mulnqprl  7885  mulnqpru  7886  mullocprlem  7887  mullocpr  7888  addcomprg  7895  mulcomprg  7897  distrlem1prl  7899  distrlem1pru  7900  distrlem4prl  7901  distrlem4pru  7902  ltprordil  7906  1idprl  7907  1idpru  7908  ltpopr  7912  ltsopr  7913  ltaddpr  7914  ltexprlemm  7917  ltexprlemopl  7918  ltexprlemlol  7919  ltexprlemopu  7920  ltexprlemupu  7921  ltexprlemdisj  7923  ltexprlemloc  7924  ltexprlemfl  7926  ltexprlemrl  7927  ltexprlemfu  7928  ltexprlemru  7929  addcanprleml  7931  addcanprlemu  7932  prplnqu  7937  recexprlemloc  7948  recexprlem1ssl  7950  recexprlem1ssu  7951  recexprlemss1l  7952  recexprlemss1u  7953  aptiprleml  7956  aptiprlemu  7957  cauappcvgprlemloc  7969  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  caucvgprlemloc  7992  caucvgprlemladdrl  7995  caucvgprprlemml  8011  caucvgprprlemloc  8020  00sr  8086  map2psrprg  8122  suplocsrlempr  8124  suplocsrlem  8125  adddir  8267  axsuploc  8348  eqle  8367  le2tri3i  8384  mul4  8407  muladd11  8408  cnegexlem3  8452  addsub12  8488  2addsub  8489  addsubeq4  8490  subadd4  8519  negcon1  8527  negdi2  8533  negsubdi2  8534  neg2sub  8535  renegcl  8536  muladd  8659  subdir  8661  gt0ne0  8703  ltnegcon1  8739  lenegcon1  8742  eqord1  8759  eqord2  8760  recexre  8854  ltmul1  8868  recexap  8929  div12ap  8970  rerecapb  9119  p1le  9125  ltmul2  9132  gt0div  9146  ge0div  9147  zlem1lt  9636  nnaddm1cl  9641  zdceq  9655  gtndiv  9676  prime  9680  msqznn  9681  btwnz  9700  uzss  9878  eluzadd  9886  nn0pzuz  9922  supinfneg  9930  infsupneg  9931  divfnzn  9956  qnegcl  9971  qreccl  9977  elpqb  9985  xaddass  10205  xleadd1a  10209  xlesubadd  10219  elico2  10273  iccss  10277  iccsupr  10302  elfz5  10354  fznn  10427  difelfznle  10473  fzoaddel  10536  elincfzoext  10542  qdceq  10608  qbtwnxr  10621  flqbi2  10655  adddivflid  10656  fldivnn0  10659  divfl0  10660  flqmulnn0  10663  fldivnn0le  10667  fldiv4p1lem1div2  10669  ceiqle  10679  flqdiv  10687  modqmulnn  10708  frecuzrdgtcl  10778  frecuzrdgsuc  10780  frecuzrdgdomlem  10783  frecuzrdgfunlem  10785  frecuzrdgsuctlem  10789  seqm1g  10840  seq3caopr2  10859  seqcaopr2g  10860  iseqf1olemkle  10863  seq3f1olemp  10881  seqf1oglem2  10886  seqf1og  10887  seq3id  10891  seq3z  10894  expap0  10935  mulexp  10944  mulexpzap  10945  expmul  10950  leexp1a  10960  expubnd  10962  zesq  11024  bernneq  11026  bernneq3  11028  modqexp  11032  facdiv  11104  facndiv  11105  faclbnd3  11109  faclbnd6  11110  bccmpl  11120  bcpasc  11132  bccl  11133  hashfibclem  11210  hashfibc  11211  seq3coll  11218  fundm2domnop  11225  wrdsymb1  11265  ccatfv0  11295  ccatrn  11301  ccat2s1cl  11325  lswccats1fst  11336  swrdspsleq  11363  pfxtrcfv  11389  pfxsuffeqwrdeq  11394  pfxlswccat  11409  wrdeqs1cat  11416  cats1un  11417  swrdccatin1  11421  pfxccatin12lem4  11422  swrdccatin2  11425  pfxccatin12  11429  swrdccat  11431  shftlem  11505  ovshftex  11508  shftval4  11517  shftf  11519  shftcan2  11524  crim  11547  mulreap  11553  remul2  11562  immul2  11569  cjexp  11582  caucvgre  11670  r19.2uz  11682  sqrtsq2  11732  absnid  11762  absexp  11768  nn0abscl  11774  abslt  11777  lenegsq  11784  cau3lem  11803  minmax  11919  xrmaxadd  11950  clim  11970  climshftlemg  11991  climcn1  11997  climcn1lem  12008  clim2ser  12026  clim2ser2  12027  iserex  12028  isermulc2  12029  climub  12033  climcaucn  12040  serf0  12041  summodclem3  12070  summodclem2a  12071  summodclem2  12072  summodc  12073  fsum3  12077  fsumf1o  12080  fisumss  12082  isumss2  12083  fsumcl2lem  12088  fsumadd  12096  fsumsplit  12097  isummulc2  12116  fsum2d  12125  fsummulc2  12138  telfsumo  12156  fsumparts  12160  hash2iun1dif1  12170  bcxmas  12179  isumshft  12180  isumsplit  12181  expcnvap0  12192  geolim  12201  geolim2  12202  cvgratnnlemmn  12215  cvgratnnlemseq  12216  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  clim2divap  12230  prodmodclem3  12265  prodmodclem2a  12266  fprodseq  12273  fprodf1o  12278  fprodmul  12281  fprodsplitdc  12286  efcllemp  12348  reefcl  12358  efcj  12363  efaddlem  12364  efexp  12372  reeftlcl  12379  eftlub  12380  efsep  12381  effsumlt  12382  eflegeo  12391  retanclap  12412  demoivre  12463  demoivreALT  12464  eirraplem  12467  dvdsval3  12481  p1modz1  12484  iddvdsexp  12505  alzdvds  12544  addmodlteqALT  12549  nnehalf  12594  nno  12596  ndvdsadd  12621  bitsp1e  12642  bitsp1o  12643  bitsinv1  12652  divgcdnnr  12676  neggcd  12683  gcdabs  12688  bezoutlemmain  12698  bezoutlemaz  12703  bezoutlembz  12704  gcdmultiplez  12721  gcdzeq  12722  dvdssq  12731  nninfctlemfo  12740  algrf  12746  algcvg  12749  algcvga  12752  algfx  12753  eucalgf  12756  eucalgcvga  12759  neglcm  12776  lcmabs  12777  lcmdvds  12780  lcmgcdeq  12784  qredeq  12797  isprm3  12819  coprm  12845  prmrp  12846  isprm6  12848  prmdvdsexpb  12850  rpexp  12854  cncongrprm  12858  sqrt2irraplemnn  12880  phibndlem  12917  phiprmpw  12923  eulerthlemh  12932  eulerthlemth  12933  fermltl  12935  prmdivdiv  12938  modprm1div  12949  m1dvdsndvds  12950  coprimeprodsq  12959  pczpre  12999  pczcl  13000  pcexp  13011  pczdvds  13016  pczndvds  13018  pczndvds2  13020  pcdvdsb  13022  pcneg  13027  pcprmpw  13036  difsqpwdvds  13040  pcmptcl  13044  pcprod  13048  fldivp1  13050  infpnlem2  13062  1arithlem4  13068  ballotfilem2  13149  ballotfilemfc0  13153  ballotfilemfcc  13154  ennnfonelemrn  13187  topnidg  13482  pwselbasb  13523  pwsplusgval  13525  pwsmulrval  13526  imasaddfnlemg  13544  imasaddflemg  13546  qusin  13556  mgmlrid  13609  mndass  13654  prdsidlem  13677  mhmco  13720  gsumsubm  13724  gsumwcl  13727  gsumwmhm  13728  grpass  13739  grpinvex  13740  dfgrp2  13757  grplid  13761  grprid  13762  grprcan  13767  grpinvssd  13807  grpinvval2  13813  prdsinvlem  13838  pwsinvg  13842  mhmid  13849  mhmmnd  13850  ghmgrp  13852  mulgnn  13860  mulgnnp1  13864  mulgnegnn  13866  mulgnnsubcl  13868  mulgz  13884  issubg2m  13923  issubg4m  13927  subgintm  13932  nmzbi  13943  eqger  13958  eqgid  13960  eqgen  13961  qusgrp  13966  qusadd  13968  qusinv  13970  qussub  13971  ghminv  13984  ghmsub  13985  ghmrn  13991  resghm2b  13996  ghmf1  14007  conjsubg  14011  conjsubgen  14012  qusghm  14016  cmncom  14036  ablsubadd  14046  ablsubsub23  14059  ghmcmn  14061  gsumfzreidx  14071  mgpress  14092  srg1expzeq1  14156  ringinvnz1ne0  14210  ringinvnzdiv  14211  dvdsrd  14256  dvdsunit  14274  unitinvcl  14285  unitinvinv  14286  unitlinv  14288  unitrinv  14289  rhmunitinv  14340  subrngintm  14374  subrg1  14393  subrguss  14398  subrginv  14399  subrgunit  14401  subrgugrp  14402  subrgintm  14405  resrhm  14410  resrhm2b  14411  lmodass  14468  lmodlcan  14469  lmod0vlid  14483  lmod0vrid  14484  lmod0vid  14485  lmodvs0  14487  lcomf  14492  lmodvnegcl  14493  lmodvnegid  14494  lmodvsubadd  14503  lmodsubid  14512  lss1d  14548  lspval  14555  lspsnel6  14573  lspsnneg  14585  sralmod  14615  dflidl2rng  14646  lidlacl  14649  dflidl2  14653  df2idl2  14674  qusmul2  14694  quscrng  14698  cnfldmulg  14741  znf1o  14816  znidom  14822  psraddcl  14852  psr0lid  14854  tgss3  14960  clsval  14993  clsss3  15012  neiss2  15024  resttop  15052  resttopon2  15060  lmconst  15098  cnima  15102  cnntri  15106  cncnp  15112  cnrest  15117  cndis  15123  lmss  15128  lmff  15131  lmtopcnp  15132  txcnp  15153  upxp  15154  uptx  15156  cnmpt11  15165  hmeoima  15192  hmeoopn  15193  hmeocld  15194  hmeontr  15195  hmeoimaf1o  15196  mettri2  15244  met0  15246  metres2  15263  blpnf  15282  xblss2ps  15286  xblss2  15287  blbas  15315  blres  15316  xmetec  15319  mopnss  15332  xmstri2  15352  mstri2  15353  xmstri  15354  mstri  15355  xmstri3  15356  mstri3  15357  msrtri  15358  mopni3  15366  unimopn  15368  comet  15381  bdxmet  15383  climcncf  15466  dedekindeulemuub  15499  dedekindicclemuub  15508  ivthdichlem  15533  dvfgg  15570  dvidlemap  15573  dvidrelem  15574  dvidsslem  15575  dvfre  15592  dvmptfsum  15607  plyadd  15633  plymul  15634  reeff1olem  15653  reeff1o  15655  sinperlem  15690  abssinper  15728  reexplog  15753  relogexp  15754  cxpexpnn  15778  cxprec  15792  rpcxpmul2  15795  abscxp  15797  wilthlem1  15865  sgmval2  15869  sgmnncl  15873  0sgmppw  15878  perfectlem1  15884  lgsdir  15925  lgsprme0  15932  lgsdinn0  15938  gausslemma2dlem3  15953  gausslemma2dlem5a  15955  2lgslem1a2  15977  2lgslem1a  15978  2lgslem3  15991  2lgs  15994  umgredgprv  16127  umgrislfupgrdom  16143  uspgredgiedg  16190  uspgriedgedg  16191  usgrislfuspgrdom  16202  usgredg2en  16207  usgredgprv  16208  usgrpredgv  16210  usgredg  16212  usgrnloopv  16213  usgredgne  16216  usgredg3  16226  usgredgedg  16239  usgredgdomord  16242  usgr1vr  16260  subgruhgrfun  16280  subupgr  16285  subumgr  16286  subusgr  16287  umgrwlknloop  16380  wlkres  16391  clwwlkccatlem  16412  clwwlkccat  16413  depindlem1  16518  depindlem2  16519  depindlem3  16520  bj-inex  16694  bj-nn0suc  16751  bj-nn0sucALT  16765  trilpolemeq1  16841  trilpolemlt1  16842  trirec0  16845  nconstwlpolemgt0  16867