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  5831  fvconst2g  5867  fex  5882  funfvima  5885  f1elima  5913  f1ocnvfv1  5917  f1ocnvfv2  5918  cocan2  5928  foeqcnvco  5930  isocnv  5951  isores2  5953  isoini  5958  isoselem  5960  f1oiso  5966  f1ofveu  6005  eloprabga  6107  suppssof1  6252  ofco  6253  offveqb  6254  ofc1g  6256  ofc2g  6257  caofid0l  6261  caofid0r  6262  caofid1  6263  caofid2  6264  fnexALT  6272  f1dmex  6277  ot1stg  6314  ot2ndg  6315  ot3rdgg  6316  eqopi  6334  2ndrn  6345  fo2ndf  6391  smores3  6458  smores2  6459  smoel  6465  smoiso  6467  tfrlem1  6473  tfrlemisucaccv  6490  tfrlemibxssdm  6492  tfrlemiubacc  6495  tfr1onlemsucaccv  6506  tfr1onlembfn  6509  tfr1onlemubacc  6511  tfr1onlemaccex  6513  tfr1onlemres  6514  tfrcllemsucaccv  6519  tfrcllembfn  6522  tfrcllemubacc  6524  tfrcllemaccex  6526  tfrcllemres  6527  tfrcl  6529  frecrdg  6573  omv2  6632  nnasuc  6643  nnmsuc  6644  nnacom  6651  nnaass  6652  nnmass  6654  nntri1  6663  nndifsnid  6674  nnmordi  6683  swoer  6729  erth  6747  riinerm  6776  qliftlem  6781  ecovass  6812  ecoviass  6813  elmapssres  6841  fvixp  6871  f1domg  6930  domssr  6950  endomtr  6963  xpsnen2g  7012  enen1  7025  enen2  7026  domen1  7027  domen2  7028  mapen  7031  mapxpen  7033  ssenen  7036  phplem1  7037  fidifsnid  7057  findcard  7076  findcard2  7077  findcard2s  7078  fidcen  7087  fieq0  7174  isotilem  7204  supisolem  7206  inflbti  7222  ordiso2  7233  djuex  7241  updjudhcoinlf  7278  updjudhcoinrg  7279  updjud  7280  ctssdccl  7309  enumctlemm  7312  nnnninf  7324  finomni  7338  pm54.43  7394  acfun  7421  ccfunen  7482  cc2lem  7484  cc3  7486  addclpi  7546  addasspig  7549  mulasspig  7551  addnidpig  7555  nnppipi  7562  ltanqi  7621  ltmnqi  7622  ltexnqq  7627  archnqq  7636  prarloclemarch2  7638  enq0sym  7651  enq0tr  7653  nqnq0pi  7657  nqnq0  7660  mulcanenq0ec  7664  addclnq0  7670  nqpnq0nq  7672  distrnq0  7678  addassnq0lemcl  7680  addassnq0  7681  prubl  7705  prarloclemlt  7712  genpdf  7727  genipv  7728  genpelvl  7731  genpelvu  7732  genpml  7736  genpmu  7737  genprndl  7740  genprndu  7741  genpassl  7743  genpassu  7744  genpassg  7745  addnqprl  7748  addnqpru  7749  addlocpr  7755  nqprm  7761  nqprl  7770  nqpru  7771  mulnqprl  7787  mulnqpru  7788  mullocprlem  7789  mullocpr  7790  addcomprg  7797  mulcomprg  7799  distrlem1prl  7801  distrlem1pru  7802  distrlem4prl  7803  distrlem4pru  7804  ltprordil  7808  1idprl  7809  1idpru  7810  ltpopr  7814  ltsopr  7815  ltaddpr  7816  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  prplnqu  7839  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  recexprlemss1u  7855  aptiprleml  7858  aptiprlemu  7859  cauappcvgprlemloc  7871  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemloc  7894  caucvgprlemladdrl  7897  caucvgprprlemml  7913  caucvgprprlemloc  7922  00sr  7988  map2psrprg  8024  suplocsrlempr  8026  suplocsrlem  8027  adddir  8169  axsuploc  8251  eqle  8270  le2tri3i  8287  mul4  8310  muladd11  8311  cnegexlem3  8355  addsub12  8391  2addsub  8392  addsubeq4  8393  subadd4  8422  negcon1  8430  negdi2  8436  negsubdi2  8437  neg2sub  8438  renegcl  8439  muladd  8562  subdir  8564  gt0ne0  8606  ltnegcon1  8642  lenegcon1  8645  eqord1  8662  eqord2  8663  recexre  8757  ltmul1  8771  recexap  8832  div12ap  8873  rerecapb  9022  p1le  9028  ltmul2  9035  gt0div  9049  ge0div  9050  zlem1lt  9535  nnaddm1cl  9540  zdceq  9554  gtndiv  9574  prime  9578  msqznn  9579  btwnz  9598  uzss  9776  eluzadd  9784  nn0pzuz  9820  supinfneg  9828  infsupneg  9829  divfnzn  9854  qnegcl  9869  qreccl  9875  elpqb  9883  xaddass  10103  xleadd1a  10107  xlesubadd  10117  elico2  10171  iccss  10175  iccsupr  10200  elfz5  10251  fznn  10323  difelfznle  10369  fzoaddel  10431  elincfzoext  10437  qdceq  10503  qbtwnxr  10516  flqbi2  10550  adddivflid  10551  fldivnn0  10554  divfl0  10555  flqmulnn0  10558  fldivnn0le  10562  fldiv4p1lem1div2  10564  ceiqle  10574  flqdiv  10582  modqmulnn  10603  frecuzrdgtcl  10673  frecuzrdgsuc  10675  frecuzrdgdomlem  10678  frecuzrdgfunlem  10680  frecuzrdgsuctlem  10684  seqm1g  10735  seq3caopr2  10754  seqcaopr2g  10755  iseqf1olemkle  10758  seq3f1olemp  10776  seqf1oglem2  10781  seqf1og  10782  seq3id  10786  seq3z  10789  expap0  10830  mulexp  10839  mulexpzap  10840  expmul  10845  leexp1a  10855  expubnd  10857  zesq  10919  bernneq  10921  bernneq3  10923  modqexp  10927  facdiv  10999  facndiv  11000  faclbnd3  11004  faclbnd6  11005  bccmpl  11015  bcpasc  11027  bccl  11028  seq3coll  11105  fundm2domnop  11109  wrdsymb1  11149  ccatfv0  11179  ccatrn  11185  ccat2s1cl  11209  lswccats1fst  11220  swrdspsleq  11247  pfxtrcfv  11273  pfxsuffeqwrdeq  11278  pfxlswccat  11293  wrdeqs1cat  11300  cats1un  11301  swrdccatin1  11305  pfxccatin12lem4  11306  swrdccatin2  11309  pfxccatin12  11313  swrdccat  11315  shftlem  11376  ovshftex  11379  shftval4  11388  shftf  11390  shftcan2  11395  crim  11418  mulreap  11424  remul2  11433  immul2  11440  cjexp  11453  caucvgre  11541  r19.2uz  11553  sqrtsq2  11603  absnid  11633  absexp  11639  nn0abscl  11645  abslt  11648  lenegsq  11655  cau3lem  11674  minmax  11790  xrmaxadd  11821  clim  11841  climshftlemg  11862  climcn1  11868  climcn1lem  11879  clim2ser  11897  clim2ser2  11898  iserex  11899  isermulc2  11900  climub  11904  climcaucn  11911  serf0  11912  summodclem3  11940  summodclem2a  11941  summodclem2  11942  summodc  11943  fsum3  11947  fsumf1o  11950  fisumss  11952  isumss2  11953  fsumcl2lem  11958  fsumadd  11966  fsumsplit  11967  isummulc2  11986  fsum2d  11995  fsummulc2  12008  telfsumo  12026  fsumparts  12030  hash2iun1dif1  12040  bcxmas  12049  isumshft  12050  isumsplit  12051  expcnvap0  12062  geolim  12071  geolim2  12072  cvgratnnlemmn  12085  cvgratnnlemseq  12086  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  clim2divap  12100  prodmodclem3  12135  prodmodclem2a  12136  fprodseq  12143  fprodf1o  12148  fprodmul  12151  fprodsplitdc  12156  efcllemp  12218  reefcl  12228  efcj  12233  efaddlem  12234  efexp  12242  reeftlcl  12249  eftlub  12250  efsep  12251  effsumlt  12252  eflegeo  12261  retanclap  12282  demoivre  12333  demoivreALT  12334  eirraplem  12337  dvdsval3  12351  p1modz1  12354  iddvdsexp  12375  alzdvds  12414  addmodlteqALT  12419  nnehalf  12464  nno  12466  ndvdsadd  12491  bitsp1e  12512  bitsp1o  12513  bitsinv1  12522  divgcdnnr  12546  neggcd  12553  gcdabs  12558  bezoutlemmain  12568  bezoutlemaz  12573  bezoutlembz  12574  gcdmultiplez  12591  gcdzeq  12592  dvdssq  12601  nninfctlemfo  12610  algrf  12616  algcvg  12619  algcvga  12622  algfx  12623  eucalgf  12626  eucalgcvga  12629  neglcm  12646  lcmabs  12647  lcmdvds  12650  lcmgcdeq  12654  qredeq  12667  isprm3  12689  coprm  12715  prmrp  12716  isprm6  12718  prmdvdsexpb  12720  rpexp  12724  cncongrprm  12728  sqrt2irraplemnn  12750  phibndlem  12787  phiprmpw  12793  eulerthlemh  12802  eulerthlemth  12803  fermltl  12805  prmdivdiv  12808  modprm1div  12819  m1dvdsndvds  12820  coprimeprodsq  12829  pczpre  12869  pczcl  12870  pcexp  12881  pczdvds  12886  pczndvds  12888  pczndvds2  12890  pcdvdsb  12892  pcneg  12897  pcprmpw  12906  difsqpwdvds  12910  pcmptcl  12914  pcprod  12918  fldivp1  12920  infpnlem2  12932  1arithlem4  12938  ennnfonelemrn  13039  topnidg  13334  pwselbasb  13375  pwsplusgval  13377  pwsmulrval  13378  imasaddfnlemg  13396  imasaddflemg  13398  qusin  13408  mgmlrid  13461  mndass  13506  prdsidlem  13529  mhmco  13572  gsumsubm  13576  gsumwcl  13579  gsumwmhm  13580  grpass  13591  grpinvex  13592  dfgrp2  13609  grplid  13613  grprid  13614  grprcan  13619  grpinvssd  13659  grpinvval2  13665  prdsinvlem  13690  pwsinvg  13694  mhmid  13701  mhmmnd  13702  ghmgrp  13704  mulgnn  13712  mulgnnp1  13716  mulgnegnn  13718  mulgnnsubcl  13720  mulgz  13736  issubg2m  13775  issubg4m  13779  subgintm  13784  nmzbi  13795  eqger  13810  eqgid  13812  eqgen  13813  qusgrp  13818  qusadd  13820  qusinv  13822  qussub  13823  ghminv  13836  ghmsub  13837  ghmrn  13843  resghm2b  13848  ghmf1  13859  conjsubg  13863  conjsubgen  13864  qusghm  13868  cmncom  13888  ablsubadd  13898  ablsubsub23  13911  ghmcmn  13913  gsumfzreidx  13923  mgpress  13943  srg1expzeq1  14007  ringinvnz1ne0  14061  ringinvnzdiv  14062  dvdsrd  14107  dvdsunit  14125  unitinvcl  14136  unitinvinv  14137  unitlinv  14139  unitrinv  14140  rhmunitinv  14191  subrngintm  14225  subrg1  14244  subrguss  14249  subrginv  14250  subrgunit  14252  subrgugrp  14253  subrgintm  14256  resrhm  14261  resrhm2b  14262  lmodass  14316  lmodlcan  14317  lmod0vlid  14331  lmod0vrid  14332  lmod0vid  14333  lmodvs0  14335  lcomf  14340  lmodvnegcl  14341  lmodvnegid  14342  lmodvsubadd  14351  lmodsubid  14360  lss1d  14396  lspval  14403  lspsnel6  14421  lspsnneg  14433  sralmod  14463  dflidl2rng  14494  lidlacl  14497  dflidl2  14501  df2idl2  14522  qusmul2  14542  quscrng  14546  cnfldmulg  14589  znf1o  14664  znidom  14670  psraddcl  14693  psr0lid  14695  tgss3  14801  clsval  14834  clsss3  14853  neiss2  14865  resttop  14893  resttopon2  14901  lmconst  14939  cnima  14943  cnntri  14947  cncnp  14953  cnrest  14958  cndis  14964  lmss  14969  lmff  14972  lmtopcnp  14973  txcnp  14994  upxp  14995  uptx  14997  cnmpt11  15006  hmeoima  15033  hmeoopn  15034  hmeocld  15035  hmeontr  15036  hmeoimaf1o  15037  mettri2  15085  met0  15087  metres2  15104  blpnf  15123  xblss2ps  15127  xblss2  15128  blbas  15156  blres  15157  xmetec  15160  mopnss  15173  xmstri2  15193  mstri2  15194  xmstri  15195  mstri  15196  xmstri3  15197  mstri3  15198  msrtri  15199  mopni3  15207  unimopn  15209  comet  15222  bdxmet  15224  climcncf  15307  dedekindeulemuub  15340  dedekindicclemuub  15349  ivthdichlem  15374  dvfgg  15411  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvfre  15433  dvmptfsum  15448  plyadd  15474  plymul  15475  reeff1olem  15494  reeff1o  15496  sinperlem  15531  abssinper  15569  reexplog  15594  relogexp  15595  cxpexpnn  15619  cxprec  15633  rpcxpmul2  15636  abscxp  15638  wilthlem1  15703  sgmval2  15707  sgmnncl  15711  0sgmppw  15716  perfectlem1  15722  lgsdir  15763  lgsprme0  15770  lgsdinn0  15776  gausslemma2dlem3  15791  gausslemma2dlem5a  15793  2lgslem1a2  15815  2lgslem1a  15816  2lgslem3  15829  2lgs  15832  umgredgprv  15965  umgrislfupgrdom  15981  uspgredgiedg  16028  uspgriedgedg  16029  usgrislfuspgrdom  16040  usgredg2en  16045  usgredgprv  16046  usgrpredgv  16048  usgredg  16050  usgrnloopv  16051  usgredgne  16054  usgredg3  16064  usgredgedg  16077  usgredgdomord  16080  usgr1vr  16098  subgruhgrfun  16118  subupgr  16123  subumgr  16124  subusgr  16125  umgrwlknloop  16218  wlkres  16229  clwwlkccatlem  16250  clwwlkccat  16251  bj-inex  16502  bj-nn0suc  16559  bj-nn0sucALT  16573  trilpolemeq1  16644  trilpolemlt1  16645  trirec0  16648  nconstwlpolemgt0  16668