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  940  3adantl1  1155  3adantl2  1156  3adantl3  1157  syl3anl1  1297  syl3anl3  1299  syl3anl  1300  stoic3  1442  eupick  2117  csbiebt  3111  csbnestgf  3124  reuss2  3430  mpteq12  4101  otexg  4248  opelopabt  4280  sonr  4335  sotr  4336  issod  4337  so2nr  4339  so3nr  4340  ordelss  4397  onelon  4402  elrnmpt1s  4895  iota2  5225  funeu  5260  imadif  5315  fnbr  5337  feu  5417  f1ss  5446  f1ssres  5449  f1resf1  5450  dffo2  5461  foco  5467  foun  5499  fun11iun  5501  ffoss  5512  funbrfv  5575  fvco3  5608  fvopab6  5633  funfvbrb  5650  elpreima  5656  ffvelcdm  5670  ffvelcdmda  5672  dffo4  5685  fmptco  5703  fsn2  5711  fvconst2g  5751  fex  5766  funfvima  5769  f1elima  5795  f1ocnvfv1  5799  f1ocnvfv2  5800  cocan2  5810  foeqcnvco  5812  isocnv  5833  isores2  5835  isoini  5840  isoselem  5842  f1oiso  5848  f1ofveu  5884  eloprabga  5983  suppssof1  6124  ofco  6125  offveqb  6126  fnexALT  6136  f1dmex  6141  ot1stg  6177  ot2ndg  6178  ot3rdgg  6179  eqopi  6197  2ndrn  6208  fo2ndf  6252  smores3  6318  smores2  6319  smoel  6325  smoiso  6327  tfrlem1  6333  tfrlemisucaccv  6350  tfrlemibxssdm  6352  tfrlemiubacc  6355  tfr1onlemsucaccv  6366  tfr1onlembfn  6369  tfr1onlemubacc  6371  tfr1onlemaccex  6373  tfr1onlemres  6374  tfrcllemsucaccv  6379  tfrcllembfn  6382  tfrcllemubacc  6384  tfrcllemaccex  6386  tfrcllemres  6387  tfrcl  6389  frecrdg  6433  omv2  6490  nnasuc  6501  nnmsuc  6502  nnacom  6509  nnaass  6510  nnmass  6512  nntri1  6521  nndifsnid  6532  nnmordi  6541  swoer  6587  erth  6605  riinerm  6634  qliftlem  6639  ecovass  6670  ecoviass  6671  elmapssres  6699  fvixp  6729  f1domg  6784  endomtr  6816  xpsnen2g  6855  enen1  6868  enen2  6869  domen1  6870  domen2  6871  mapen  6874  mapxpen  6876  ssenen  6879  phplem1  6880  fidifsnid  6899  findcard  6916  findcard2  6917  findcard2s  6918  fieq0  7005  isotilem  7035  supisolem  7037  inflbti  7053  ordiso2  7064  djuex  7072  updjudhcoinlf  7109  updjudhcoinrg  7110  updjud  7111  ctssdccl  7140  enumctlemm  7143  nnnninf  7154  finomni  7168  pm54.43  7219  acfun  7236  ccfunen  7293  cc2lem  7295  cc3  7297  addclpi  7356  addasspig  7359  mulasspig  7361  addnidpig  7365  nnppipi  7372  ltanqi  7431  ltmnqi  7432  ltexnqq  7437  archnqq  7446  prarloclemarch2  7448  enq0sym  7461  enq0tr  7463  nqnq0pi  7467  nqnq0  7470  mulcanenq0ec  7474  addclnq0  7480  nqpnq0nq  7482  distrnq0  7488  addassnq0lemcl  7490  addassnq0  7491  prubl  7515  prarloclemlt  7522  genpdf  7537  genipv  7538  genpelvl  7541  genpelvu  7542  genpml  7546  genpmu  7547  genprndl  7550  genprndu  7551  genpassl  7553  genpassu  7554  genpassg  7555  addnqprl  7558  addnqpru  7559  addlocpr  7565  nqprm  7571  nqprl  7580  nqpru  7581  mulnqprl  7597  mulnqpru  7598  mullocprlem  7599  mullocpr  7600  addcomprg  7607  mulcomprg  7609  distrlem1prl  7611  distrlem1pru  7612  distrlem4prl  7613  distrlem4pru  7614  ltprordil  7618  1idprl  7619  1idpru  7620  ltpopr  7624  ltsopr  7625  ltaddpr  7626  ltexprlemm  7629  ltexprlemopl  7630  ltexprlemlol  7631  ltexprlemopu  7632  ltexprlemupu  7633  ltexprlemdisj  7635  ltexprlemloc  7636  ltexprlemfl  7638  ltexprlemrl  7639  ltexprlemfu  7640  ltexprlemru  7641  addcanprleml  7643  addcanprlemu  7644  prplnqu  7649  recexprlemloc  7660  recexprlem1ssl  7662  recexprlem1ssu  7663  recexprlemss1l  7664  recexprlemss1u  7665  aptiprleml  7668  aptiprlemu  7669  cauappcvgprlemloc  7681  cauappcvgprlemladdru  7685  cauappcvgprlemladdrl  7686  caucvgprlemloc  7704  caucvgprlemladdrl  7707  caucvgprprlemml  7723  caucvgprprlemloc  7732  00sr  7798  map2psrprg  7834  suplocsrlempr  7836  suplocsrlem  7837  adddir  7978  axsuploc  8060  eqle  8079  le2tri3i  8096  mul4  8119  muladd11  8120  cnegexlem3  8164  addsub12  8200  2addsub  8201  addsubeq4  8202  subadd4  8231  negcon1  8239  negdi2  8245  negsubdi2  8246  neg2sub  8247  renegcl  8248  muladd  8371  subdir  8373  gt0ne0  8414  ltnegcon1  8450  lenegcon1  8453  eqord1  8470  eqord2  8471  recexre  8565  ltmul1  8579  recexap  8640  div12ap  8681  rerecapb  8830  p1le  8836  ltmul2  8843  gt0div  8857  ge0div  8858  zlem1lt  9339  nnaddm1cl  9344  zdceq  9358  gtndiv  9378  prime  9382  msqznn  9383  btwnz  9402  uzss  9578  eluzadd  9586  nn0pzuz  9617  supinfneg  9625  infsupneg  9626  divfnzn  9651  qnegcl  9666  qreccl  9672  elpqb  9679  xaddass  9899  xleadd1a  9903  xlesubadd  9913  elico2  9967  iccss  9971  iccsupr  9996  elfz5  10047  fznn  10119  difelfznle  10165  fzoaddel  10222  qdceq  10277  qbtwnxr  10288  flqbi2  10322  adddivflid  10323  fldivnn0  10326  divfl0  10327  flqmulnn0  10330  fldivnn0le  10334  fldiv4p1lem1div2  10336  ceiqle  10344  flqdiv  10352  modqmulnn  10373  frecuzrdgtcl  10443  frecuzrdgsuc  10445  frecuzrdgdomlem  10448  frecuzrdgfunlem  10450  frecuzrdgsuctlem  10454  seq3caopr2  10513  iseqf1olemkle  10515  seq3f1olemp  10533  seq3id  10539  seq3z  10542  expap0  10581  mulexp  10590  mulexpzap  10591  expmul  10596  leexp1a  10606  expubnd  10608  zesq  10670  bernneq  10672  bernneq3  10674  modqexp  10678  facdiv  10750  facndiv  10751  faclbnd3  10755  faclbnd6  10756  bccmpl  10766  bcpasc  10778  bccl  10779  seq3coll  10854  shftlem  10857  ovshftex  10860  shftval4  10869  shftf  10871  shftcan2  10876  crim  10899  mulreap  10905  remul2  10914  immul2  10921  cjexp  10934  caucvgre  11022  r19.2uz  11034  sqrtsq2  11084  absnid  11114  absexp  11120  nn0abscl  11126  abslt  11129  lenegsq  11136  cau3lem  11155  minmax  11270  xrmaxadd  11301  clim  11321  climshftlemg  11342  climcn1  11348  climcn1lem  11359  clim2ser  11377  clim2ser2  11378  iserex  11379  isermulc2  11380  climub  11384  climcaucn  11391  serf0  11392  summodclem3  11420  summodclem2a  11421  summodclem2  11422  summodc  11423  fsum3  11427  fsumf1o  11430  fisumss  11432  isumss2  11433  fsumcl2lem  11438  fsumadd  11446  fsumsplit  11447  isummulc2  11466  fsum2d  11475  fsummulc2  11488  telfsumo  11506  fsumparts  11510  hash2iun1dif1  11520  bcxmas  11529  isumshft  11530  isumsplit  11531  expcnvap0  11542  geolim  11551  geolim2  11552  cvgratnnlemmn  11565  cvgratnnlemseq  11566  mertenslemi1  11575  mertenslem2  11576  mertensabs  11577  clim2divap  11580  prodmodclem3  11615  prodmodclem2a  11616  fprodseq  11623  fprodf1o  11628  fprodmul  11631  fprodsplitdc  11636  efcllemp  11698  reefcl  11708  efcj  11713  efaddlem  11714  efexp  11722  reeftlcl  11729  eftlub  11730  efsep  11731  effsumlt  11732  eflegeo  11741  retanclap  11762  demoivre  11812  demoivreALT  11813  eirraplem  11816  dvdsval3  11830  p1modz1  11833  iddvdsexp  11854  alzdvds  11892  addmodlteqALT  11897  nnehalf  11941  nno  11943  ndvdsadd  11968  divgcdnnr  12009  neggcd  12016  gcdabs  12021  bezoutlemmain  12031  bezoutlemaz  12036  bezoutlembz  12037  gcdmultiplez  12054  gcdzeq  12055  dvdssq  12064  algrf  12077  algcvg  12080  algcvga  12083  algfx  12084  eucalgf  12087  eucalgcvga  12090  neglcm  12107  lcmabs  12108  lcmdvds  12111  lcmgcdeq  12115  qredeq  12128  isprm3  12150  coprm  12176  prmrp  12177  isprm6  12179  prmdvdsexpb  12181  rpexp  12185  cncongrprm  12189  sqrt2irraplemnn  12211  phibndlem  12248  phiprmpw  12254  eulerthlemh  12263  eulerthlemth  12264  fermltl  12266  prmdivdiv  12269  modprm1div  12279  m1dvdsndvds  12280  coprimeprodsq  12289  pczpre  12329  pczcl  12330  pcexp  12341  pczdvds  12346  pczndvds  12348  pczndvds2  12350  pcdvdsb  12352  pcneg  12357  pcprmpw  12366  difsqpwdvds  12370  pcmptcl  12374  pcprod  12378  fldivp1  12380  infpnlem2  12392  1arithlem4  12398  ennnfonelemrn  12470  topnidg  12757  imasaddfnlemg  12791  imasaddflemg  12793  qusin  12803  mgmlrid  12855  mndass  12885  mhmco  12942  grpass  12954  grpinvex  12955  dfgrp2  12971  grplid  12975  grprid  12976  grprcan  12981  grpinvssd  13021  grpinvval2  13027  mhmid  13057  mhmmnd  13058  ghmgrp  13060  mulgnn  13068  mulgnnp1  13070  mulgnegnn  13072  mulgnnsubcl  13074  mulgz  13090  issubg2m  13128  issubg4m  13132  subgintm  13137  nmzbi  13148  eqger  13163  eqgid  13165  eqgen  13166  qusgrp  13171  qusadd  13173  qusinv  13175  qussub  13176  ghminv  13189  ghmsub  13190  ghmrn  13196  resghm2b  13201  ghmf1  13212  conjsubg  13216  conjsubgen  13217  qusghm  13221  cmncom  13241  ablsubadd  13251  ablsubsub23  13264  ghmcmn  13265  mgpress  13285  srg1expzeq1  13349  ringinvnz1ne0  13401  ringinvnzdiv  13402  dvdsrd  13444  dvdsunit  13462  unitinvcl  13473  unitinvinv  13474  unitlinv  13476  unitrinv  13477  rhmunitinv  13528  subrngintm  13559  subrg1  13578  subrguss  13583  subrginv  13584  subrgunit  13586  subrgugrp  13587  subrgintm  13590  lmodass  13619  lmodlcan  13620  lmod0vlid  13634  lmod0vrid  13635  lmod0vid  13636  lmodvs0  13638  lcomf  13643  lmodvnegcl  13644  lmodvnegid  13645  lmodvsubadd  13654  lmodsubid  13663  lss1d  13699  lspval  13706  lspsnel6  13724  lspsnneg  13736  sralmod  13766  dflidl2rng  13797  lidlacl  13800  dflidl2  13804  df2idl2  13824  qusmul2  13843  quscrng  13847  cnfldmulg  13879  tgss3  14035  clsval  14068  clsss3  14087  neiss2  14099  resttop  14127  resttopon2  14135  lmconst  14173  cnima  14177  cnntri  14181  cncnp  14187  cnrest  14192  cndis  14198  lmss  14203  lmff  14206  lmtopcnp  14207  txcnp  14228  upxp  14229  uptx  14231  cnmpt11  14240  hmeoima  14267  hmeoopn  14268  hmeocld  14269  hmeontr  14270  hmeoimaf1o  14271  mettri2  14319  met0  14321  metres2  14338  blpnf  14357  xblss2ps  14361  xblss2  14362  blbas  14390  blres  14391  xmetec  14394  mopnss  14407  xmstri2  14427  mstri2  14428  xmstri  14429  mstri  14430  xmstri3  14431  mstri3  14432  msrtri  14433  mopni3  14441  unimopn  14443  comet  14456  bdxmet  14458  climcncf  14528  dedekindeulemuub  14552  dedekindicclemuub  14561  dvfgg  14614  dvidlemap  14617  dvfre  14631  reeff1olem  14649  reeff1o  14651  sinperlem  14686  abssinper  14724  reexplog  14749  relogexp  14750  cxpexpnn  14774  cxprec  14788  abscxp  14792  wilthlem1  14855  lgsdir  14894  lgsprme0  14901  lgsdinn0  14907  bj-inex  15117  bj-nn0suc  15174  bj-nn0sucALT  15188  trilpolemeq1  15247  trilpolemlt1  15248  trirec0  15251  nconstwlpolemgt0  15271