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  2124  csbiebt  3124  csbnestgf  3137  reuss2  3444  mpteq12  4117  otexg  4264  opelopabt  4297  sonr  4353  sotr  4354  issod  4355  so2nr  4357  so3nr  4358  ordelss  4415  onelon  4420  elrnmpt1s  4917  iota2  5249  funeu  5284  imadif  5339  fnbr  5363  feu  5443  f1ss  5472  f1ssres  5475  f1resf1  5476  dffo2  5487  foco  5494  foun  5526  fun11iun  5528  ffoss  5539  funbrfv  5602  fvco3  5635  fvopab6  5661  funfvbrb  5678  elpreima  5684  ffvelcdm  5698  ffvelcdmda  5700  dffo4  5713  fmptco  5731  fsn2  5739  fvconst2g  5779  fex  5794  funfvima  5797  f1elima  5823  f1ocnvfv1  5827  f1ocnvfv2  5828  cocan2  5838  foeqcnvco  5840  isocnv  5861  isores2  5863  isoini  5868  isoselem  5870  f1oiso  5876  f1ofveu  5913  eloprabga  6013  suppssof1  6157  ofco  6158  offveqb  6159  ofc1g  6161  ofc2g  6162  caofid0l  6166  caofid0r  6167  caofid1  6168  caofid2  6169  fnexALT  6177  f1dmex  6182  ot1stg  6219  ot2ndg  6220  ot3rdgg  6221  eqopi  6239  2ndrn  6250  fo2ndf  6294  smores3  6360  smores2  6361  smoel  6367  smoiso  6369  tfrlem1  6375  tfrlemisucaccv  6392  tfrlemibxssdm  6394  tfrlemiubacc  6397  tfr1onlemsucaccv  6408  tfr1onlembfn  6411  tfr1onlemubacc  6413  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucaccv  6421  tfrcllembfn  6424  tfrcllemubacc  6426  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  frecrdg  6475  omv2  6532  nnasuc  6543  nnmsuc  6544  nnacom  6551  nnaass  6552  nnmass  6554  nntri1  6563  nndifsnid  6574  nnmordi  6583  swoer  6629  erth  6647  riinerm  6676  qliftlem  6681  ecovass  6712  ecoviass  6713  elmapssres  6741  fvixp  6771  f1domg  6826  endomtr  6858  xpsnen2g  6897  enen1  6910  enen2  6911  domen1  6912  domen2  6913  mapen  6916  mapxpen  6918  ssenen  6921  phplem1  6922  fidifsnid  6941  findcard  6958  findcard2  6959  findcard2s  6960  fieq0  7051  isotilem  7081  supisolem  7083  inflbti  7099  ordiso2  7110  djuex  7118  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  ctssdccl  7186  enumctlemm  7189  nnnninf  7201  finomni  7215  pm54.43  7269  acfun  7290  ccfunen  7347  cc2lem  7349  cc3  7351  addclpi  7411  addasspig  7414  mulasspig  7416  addnidpig  7420  nnppipi  7427  ltanqi  7486  ltmnqi  7487  ltexnqq  7492  archnqq  7501  prarloclemarch2  7503  enq0sym  7516  enq0tr  7518  nqnq0pi  7522  nqnq0  7525  mulcanenq0ec  7529  addclnq0  7535  nqpnq0nq  7537  distrnq0  7543  addassnq0lemcl  7545  addassnq0  7546  prubl  7570  prarloclemlt  7577  genpdf  7592  genipv  7593  genpelvl  7596  genpelvu  7597  genpml  7601  genpmu  7602  genprndl  7605  genprndu  7606  genpassl  7608  genpassu  7609  genpassg  7610  addnqprl  7613  addnqpru  7614  addlocpr  7620  nqprm  7626  nqprl  7635  nqpru  7636  mulnqprl  7652  mulnqpru  7653  mullocprlem  7654  mullocpr  7655  addcomprg  7662  mulcomprg  7664  distrlem1prl  7666  distrlem1pru  7667  distrlem4prl  7668  distrlem4pru  7669  ltprordil  7673  1idprl  7674  1idpru  7675  ltpopr  7679  ltsopr  7680  ltaddpr  7681  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemlol  7686  ltexprlemopu  7687  ltexprlemupu  7688  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemfl  7693  ltexprlemrl  7694  ltexprlemfu  7695  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  prplnqu  7704  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  recexprlemss1l  7719  recexprlemss1u  7720  aptiprleml  7723  aptiprlemu  7724  cauappcvgprlemloc  7736  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemloc  7759  caucvgprlemladdrl  7762  caucvgprprlemml  7778  caucvgprprlemloc  7787  00sr  7853  map2psrprg  7889  suplocsrlempr  7891  suplocsrlem  7892  adddir  8034  axsuploc  8116  eqle  8135  le2tri3i  8152  mul4  8175  muladd11  8176  cnegexlem3  8220  addsub12  8256  2addsub  8257  addsubeq4  8258  subadd4  8287  negcon1  8295  negdi2  8301  negsubdi2  8302  neg2sub  8303  renegcl  8304  muladd  8427  subdir  8429  gt0ne0  8471  ltnegcon1  8507  lenegcon1  8510  eqord1  8527  eqord2  8528  recexre  8622  ltmul1  8636  recexap  8697  div12ap  8738  rerecapb  8887  p1le  8893  ltmul2  8900  gt0div  8914  ge0div  8915  zlem1lt  9399  nnaddm1cl  9404  zdceq  9418  gtndiv  9438  prime  9442  msqznn  9443  btwnz  9462  uzss  9639  eluzadd  9647  nn0pzuz  9678  supinfneg  9686  infsupneg  9687  divfnzn  9712  qnegcl  9727  qreccl  9733  elpqb  9741  xaddass  9961  xleadd1a  9965  xlesubadd  9975  elico2  10029  iccss  10033  iccsupr  10058  elfz5  10109  fznn  10181  difelfznle  10227  fzoaddel  10285  qdceq  10351  qbtwnxr  10364  flqbi2  10398  adddivflid  10399  fldivnn0  10402  divfl0  10403  flqmulnn0  10406  fldivnn0le  10410  fldiv4p1lem1div2  10412  ceiqle  10422  flqdiv  10430  modqmulnn  10451  frecuzrdgtcl  10521  frecuzrdgsuc  10523  frecuzrdgdomlem  10526  frecuzrdgfunlem  10528  frecuzrdgsuctlem  10532  seqm1g  10583  seq3caopr2  10602  seqcaopr2g  10603  iseqf1olemkle  10606  seq3f1olemp  10624  seqf1oglem2  10629  seqf1og  10630  seq3id  10634  seq3z  10637  expap0  10678  mulexp  10687  mulexpzap  10688  expmul  10693  leexp1a  10703  expubnd  10705  zesq  10767  bernneq  10769  bernneq3  10771  modqexp  10775  facdiv  10847  facndiv  10848  faclbnd3  10852  faclbnd6  10853  bccmpl  10863  bcpasc  10875  bccl  10876  seq3coll  10951  wrdsymb1  10988  shftlem  10998  ovshftex  11001  shftval4  11010  shftf  11012  shftcan2  11017  crim  11040  mulreap  11046  remul2  11055  immul2  11062  cjexp  11075  caucvgre  11163  r19.2uz  11175  sqrtsq2  11225  absnid  11255  absexp  11261  nn0abscl  11267  abslt  11270  lenegsq  11277  cau3lem  11296  minmax  11412  xrmaxadd  11443  clim  11463  climshftlemg  11484  climcn1  11490  climcn1lem  11501  clim2ser  11519  clim2ser2  11520  iserex  11521  isermulc2  11522  climub  11526  climcaucn  11533  serf0  11534  summodclem3  11562  summodclem2a  11563  summodclem2  11564  summodc  11565  fsum3  11569  fsumf1o  11572  fisumss  11574  isumss2  11575  fsumcl2lem  11580  fsumadd  11588  fsumsplit  11589  isummulc2  11608  fsum2d  11617  fsummulc2  11630  telfsumo  11648  fsumparts  11652  hash2iun1dif1  11662  bcxmas  11671  isumshft  11672  isumsplit  11673  expcnvap0  11684  geolim  11693  geolim2  11694  cvgratnnlemmn  11707  cvgratnnlemseq  11708  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  clim2divap  11722  prodmodclem3  11757  prodmodclem2a  11758  fprodseq  11765  fprodf1o  11770  fprodmul  11773  fprodsplitdc  11778  efcllemp  11840  reefcl  11850  efcj  11855  efaddlem  11856  efexp  11864  reeftlcl  11871  eftlub  11872  efsep  11873  effsumlt  11874  eflegeo  11883  retanclap  11904  demoivre  11955  demoivreALT  11956  eirraplem  11959  dvdsval3  11973  p1modz1  11976  iddvdsexp  11997  alzdvds  12036  addmodlteqALT  12041  nnehalf  12086  nno  12088  ndvdsadd  12113  bitsp1e  12134  bitsp1o  12135  bitsinv1  12144  divgcdnnr  12168  neggcd  12175  gcdabs  12180  bezoutlemmain  12190  bezoutlemaz  12195  bezoutlembz  12196  gcdmultiplez  12213  gcdzeq  12214  dvdssq  12223  nninfctlemfo  12232  algrf  12238  algcvg  12241  algcvga  12244  algfx  12245  eucalgf  12248  eucalgcvga  12251  neglcm  12268  lcmabs  12269  lcmdvds  12272  lcmgcdeq  12276  qredeq  12289  isprm3  12311  coprm  12337  prmrp  12338  isprm6  12340  prmdvdsexpb  12342  rpexp  12346  cncongrprm  12350  sqrt2irraplemnn  12372  phibndlem  12409  phiprmpw  12415  eulerthlemh  12424  eulerthlemth  12425  fermltl  12427  prmdivdiv  12430  modprm1div  12441  m1dvdsndvds  12442  coprimeprodsq  12451  pczpre  12491  pczcl  12492  pcexp  12503  pczdvds  12508  pczndvds  12510  pczndvds2  12512  pcdvdsb  12514  pcneg  12519  pcprmpw  12528  difsqpwdvds  12532  pcmptcl  12536  pcprod  12540  fldivp1  12542  infpnlem2  12554  1arithlem4  12560  ennnfonelemrn  12661  topnidg  12954  pwselbasb  12995  pwsplusgval  12997  pwsmulrval  12998  imasaddfnlemg  13016  imasaddflemg  13018  qusin  13028  mgmlrid  13081  mndass  13126  prdsidlem  13149  mhmco  13192  gsumsubm  13196  gsumwcl  13199  gsumwmhm  13200  grpass  13211  grpinvex  13212  dfgrp2  13229  grplid  13233  grprid  13234  grprcan  13239  grpinvssd  13279  grpinvval2  13285  prdsinvlem  13310  pwsinvg  13314  mhmid  13321  mhmmnd  13322  ghmgrp  13324  mulgnn  13332  mulgnnp1  13336  mulgnegnn  13338  mulgnnsubcl  13340  mulgz  13356  issubg2m  13395  issubg4m  13399  subgintm  13404  nmzbi  13415  eqger  13430  eqgid  13432  eqgen  13433  qusgrp  13438  qusadd  13440  qusinv  13442  qussub  13443  ghminv  13456  ghmsub  13457  ghmrn  13463  resghm2b  13468  ghmf1  13479  conjsubg  13483  conjsubgen  13484  qusghm  13488  cmncom  13508  ablsubadd  13518  ablsubsub23  13531  ghmcmn  13533  gsumfzreidx  13543  mgpress  13563  srg1expzeq1  13627  ringinvnz1ne0  13681  ringinvnzdiv  13682  dvdsrd  13726  dvdsunit  13744  unitinvcl  13755  unitinvinv  13756  unitlinv  13758  unitrinv  13759  rhmunitinv  13810  subrngintm  13844  subrg1  13863  subrguss  13868  subrginv  13869  subrgunit  13871  subrgugrp  13872  subrgintm  13875  resrhm  13880  resrhm2b  13881  lmodass  13935  lmodlcan  13936  lmod0vlid  13950  lmod0vrid  13951  lmod0vid  13952  lmodvs0  13954  lcomf  13959  lmodvnegcl  13960  lmodvnegid  13961  lmodvsubadd  13970  lmodsubid  13979  lss1d  14015  lspval  14022  lspsnel6  14040  lspsnneg  14052  sralmod  14082  dflidl2rng  14113  lidlacl  14116  dflidl2  14120  df2idl2  14141  qusmul2  14161  quscrng  14165  cnfldmulg  14208  znf1o  14283  znidom  14289  psraddcl  14308  psr0lid  14310  tgss3  14398  clsval  14431  clsss3  14450  neiss2  14462  resttop  14490  resttopon2  14498  lmconst  14536  cnima  14540  cnntri  14544  cncnp  14550  cnrest  14555  cndis  14561  lmss  14566  lmff  14569  lmtopcnp  14570  txcnp  14591  upxp  14592  uptx  14594  cnmpt11  14603  hmeoima  14630  hmeoopn  14631  hmeocld  14632  hmeontr  14633  hmeoimaf1o  14634  mettri2  14682  met0  14684  metres2  14701  blpnf  14720  xblss2ps  14724  xblss2  14725  blbas  14753  blres  14754  xmetec  14757  mopnss  14770  xmstri2  14790  mstri2  14791  xmstri  14792  mstri  14793  xmstri3  14794  mstri3  14795  msrtri  14796  mopni3  14804  unimopn  14806  comet  14819  bdxmet  14821  climcncf  14904  dedekindeulemuub  14937  dedekindicclemuub  14946  ivthdichlem  14971  dvfgg  15008  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvfre  15030  dvmptfsum  15045  plyadd  15071  plymul  15072  reeff1olem  15091  reeff1o  15093  sinperlem  15128  abssinper  15166  reexplog  15191  relogexp  15192  cxpexpnn  15216  cxprec  15230  rpcxpmul2  15233  abscxp  15235  wilthlem1  15300  sgmval2  15304  sgmnncl  15308  0sgmppw  15313  perfectlem1  15319  lgsdir  15360  lgsprme0  15367  lgsdinn0  15373  gausslemma2dlem3  15388  gausslemma2dlem5a  15390  2lgslem1a2  15412  2lgslem1a  15413  2lgslem3  15426  2lgs  15429  bj-inex  15637  bj-nn0suc  15694  bj-nn0sucALT  15708  trilpolemeq1  15771  trilpolemlt1  15772  trirec0  15775  nconstwlpolemgt0  15795