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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylanb  284  sylanbr  285  syl2an  289  sylanl1  406  sylanl2  407  mpanl1  438  mpanl2  439  syldanl  453  adantll  480  adantlr  481  ancom1s  575  pm4.55dc  951  dfifp2dc  994  3adantl1  1184  3adantl2  1185  3adantl3  1186  syl3anl1  1326  syl3anl3  1328  syl3anl  1329  stoic3  1480  eupick  2166  csbiebt  3187  csbnestgf  3200  reuss2  3513  mpteq12  4214  otexg  4370  opelopabt  4404  sonr  4462  sotr  4463  issod  4464  so2nr  4466  so3nr  4467  ordelss  4524  onelon  4529  elrnmpt1s  5032  iota2  5367  funeu  5402  imadif  5461  fnbr  5485  feu  5574  f1ss  5604  f1ssres  5607  f1resf1  5608  dffo2  5619  foco  5626  foun  5658  fun11iun  5660  ffoss  5672  funbrfv  5739  fvco3  5776  fvopab6  5805  funfvbrb  5822  elpreima  5828  ffvelcdm  5841  ffvelcdmda  5843  dffo4  5856  fmptco  5874  fsn2  5882  fncofn  5893  fvconst2g  5929  fex  5947  funfvima  5950  f1elima  5979  f1ocnvfv1  5983  f1ocnvfv2  5984  cocan2  5994  foeqcnvco  5996  isocnv  6017  isores2  6019  isoini  6024  isoselem  6026  f1oiso  6032  f1ofveu  6073  eloprabga  6175  suppssof1  6320  ofco  6321  offveqb  6322  ofc1g  6324  ofc2g  6325  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  fnexALT  6340  f1dmex  6345  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  eqopi  6406  2ndrn  6417  fo2ndf  6463  suppval1  6479  ressuppss  6494  suppssrst  6501  suppssrgst  6502  smores3  6564  smores2  6565  smoel  6571  smoiso  6573  tfrlem1  6579  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemiubacc  6601  tfr1onlemsucaccv  6612  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  frecrdg  6679  omv2  6738  nnasuc  6749  nnmsuc  6750  nnacom  6757  nnaass  6758  nnmass  6760  nntri1  6769  nndifsnid  6780  nnmordi  6789  swoer  6835  erth  6853  riinerm  6882  qliftlem  6887  ecovass  6918  ecoviass  6919  elmapssres  6954  fvixp  6985  f1domg  7044  domssr  7064  endomtr  7077  xpsnen2g  7127  enen1  7140  enen2  7141  domen1  7142  domen2  7143  mapen  7146  mapxpen  7148  ssenen  7152  phplem1  7153  fidifsnid  7173  findcard  7192  findcard2  7193  findcard2s  7194  fidcen  7203  fieq0  7310  isotilem  7346  supisolem  7348  inflbti  7364  ordiso2  7375  djuex  7383  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  ctssdccl  7451  enumctlemm  7454  nnnninf  7466  finomni  7480  pm54.43  7536  acfun  7563  ccfunen  7630  cc2lem  7632  cc3  7634  addclpi  7694  addasspig  7697  mulasspig  7699  addnidpig  7703  nnppipi  7710  ltanqi  7769  ltmnqi  7770  ltexnqq  7775  archnqq  7784  prarloclemarch2  7786  enq0sym  7799  enq0tr  7801  nqnq0pi  7805  nqnq0  7808  mulcanenq0ec  7812  addclnq0  7818  nqpnq0nq  7820  distrnq0  7826  addassnq0lemcl  7828  addassnq0  7829  prubl  7853  prarloclemlt  7860  genpdf  7875  genipv  7876  genpelvl  7879  genpelvu  7880  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  genpassl  7891  genpassu  7892  genpassg  7893  addnqprl  7896  addnqpru  7897  addlocpr  7903  nqprm  7909  nqprl  7918  nqpru  7919  mulnqprl  7935  mulnqpru  7936  mullocprlem  7937  mullocpr  7938  addcomprg  7945  mulcomprg  7947  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  ltprordil  7956  1idprl  7957  1idpru  7958  ltpopr  7962  ltsopr  7963  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  prplnqu  7987  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  aptiprleml  8006  aptiprlemu  8007  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemloc  8042  caucvgprlemladdrl  8045  caucvgprprlemml  8061  caucvgprprlemloc  8070  00sr  8136  map2psrprg  8172  suplocsrlempr  8174  suplocsrlem  8175  adddir  8317  axsuploc  8398  eqle  8417  le2tri3i  8434  mul4  8458  muladd11  8459  cnegexlem3  8503  addsub12  8539  2addsub  8540  addsubeq4  8541  subadd4  8570  negcon1  8578  negdi2  8584  negsubdi2  8585  neg2sub  8586  renegcl  8587  muladd  8711  subdir  8713  gt0ne0  8755  ltnegcon1  8791  lenegcon1  8794  eqord1  8811  eqord2  8812  recexre  8906  ltmul1  8920  recexap  8981  div12ap  9024  rerecapb  9173  p1le  9179  ltmul2  9186  gt0div  9200  ge0div  9201  zlem1lt  9701  nnaddm1cl  9706  zdceq  9720  gtndiv  9741  prime  9745  msqznn  9746  btwnz  9765  uzss  9943  eluzadd  9951  nn0pzuz  9987  supinfneg  9995  infsupneg  9996  divfnzn  10021  qnegcl  10036  qreccl  10042  elpqb  10050  xaddass  10271  xleadd1a  10275  xlesubadd  10285  elico2  10339  iccss  10343  iccsupr  10368  elfz5  10420  fznn  10496  difelfznle  10542  fzoaddel  10605  elincfzoext  10611  qdceq  10679  qbtwnxr  10692  flqbi2  10726  adddivflid  10727  fldivnn0  10730  divfl0  10731  flqmulnn0  10734  fldivnn0le  10738  fldiv4p1lem1div2  10740  ceiqle  10750  flqdiv  10758  modqmulnn  10779  frecuzrdgtcl  10849  frecuzrdgsuc  10851  frecuzrdgdomlem  10854  frecuzrdgfunlem  10856  frecuzrdgsuctlem  10860  seqm1g  10911  seq3caopr2  10930  seqcaopr2g  10931  iseqf1olemkle  10934  seq3f1olemp  10952  seqf1oglem2  10957  seqf1og  10958  seq3id  10962  seq3z  10965  expap0  11006  mulexp  11015  mulexpzap  11016  expmul  11021  leexp1a  11031  expubnd  11033  zesq  11096  bernneq  11098  bernneq3  11100  modqexp  11104  facdiv  11176  facndiv  11177  faclbnd3  11181  faclbnd6  11182  bccmpl  11192  bcpasc  11204  bccl  11205  hashfibclem  11282  hashfibc  11283  seq3coll  11294  fundm2domnop  11301  wrdsymb1  11341  ccatfv0  11371  ccatrn  11377  ccat2s1cl  11401  lswccats1fst  11412  swrdspsleq  11439  pfxtrcfv  11465  pfxsuffeqwrdeq  11470  pfxlswccat  11485  wrdeqs1cat  11492  cats1un  11493  swrdccatin1  11497  pfxccatin12lem4  11498  swrdccatin2  11501  pfxccatin12  11505  swrdccat  11507  shftlem  11581  ovshftex  11584  shftval4  11593  shftf  11595  shftcan2  11600  crim  11623  mulreap  11629  remul2  11638  immul2  11645  cjexp  11658  caucvgre  11747  r19.2uz  11759  sqrtsq2  11809  absnid  11839  absexp  11845  nn0abscl  11851  abslt  11854  lenegsq  11861  cau3lem  11880  minmax  11996  xrmaxadd  12027  clim  12047  climshftlemg  12068  climcn1  12074  climcn1lem  12085  clim2ser  12103  clim2ser2  12104  iserex  12105  isermulc2  12106  climub  12110  climcaucn  12117  serf0  12118  summodclem3  12147  summodclem2a  12148  summodclem2  12149  summodc  12150  fsum3  12154  fsumf1o  12157  fisumss  12159  isumss2  12160  fsumcl2lem  12165  fsumadd  12173  fsumsplit  12174  isummulc2  12193  fsum2d  12202  fsummulc2  12215  telfsumo  12233  fsumparts  12237  hash2iun1dif1  12247  bcxmas  12256  isumshft  12257  isumsplit  12258  expcnvap0  12269  geolim  12278  geolim2  12279  cvgratnnlemmn  12292  cvgratnnlemseq  12293  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  clim2divap  12307  prodmodclem3  12342  prodmodclem2a  12343  fprodseq  12350  fprodf1o  12355  fprodmul  12358  fprodsplitdc  12363  efcllemp  12425  reefcl  12435  efcj  12440  efaddlem  12441  efexp  12449  reeftlcl  12456  eftlub  12457  efsep  12458  effsumlt  12459  eflegeo  12468  retanclap  12489  demoivre  12540  demoivreALT  12541  eirraplem  12544  dvdsval3  12558  p1modz1  12561  iddvdsexp  12582  alzdvds  12621  addmodlteqALT  12626  nnehalf  12671  nno  12673  ndvdsadd  12698  bitsp1e  12719  bitsp1o  12720  bitsinv1  12729  divgcdnnr  12753  neggcd  12760  gcdabs  12765  bezoutlemmain  12775  bezoutlemaz  12780  bezoutlembz  12781  gcdmultiplez  12798  gcdzeq  12799  dvdssq  12808  nninfctlemfo  12817  algrf  12823  algcvg  12826  algcvga  12829  algfx  12830  eucalgf  12833  eucalgcvga  12836  neglcm  12853  lcmabs  12854  lcmdvds  12857  lcmgcdeq  12861  qredeq  12874  isprm3  12896  coprm  12922  prmrp  12923  isprm6  12925  prmdvdsexpb  12927  rpexp  12931  cncongrprm  12935  sqrt2irraplemnn  12957  phibndlem  12994  phiprmpw  13000  eulerthlemh  13009  eulerthlemth  13010  fermltl  13012  prmdivdiv  13015  modprm1div  13026  m1dvdsndvds  13027  coprimeprodsq  13036  pczpre  13076  pczcl  13077  pcexp  13088  pczdvds  13093  pczndvds  13095  pczndvds2  13097  pcdvdsb  13099  pcneg  13104  pcprmpw  13113  difsqpwdvds  13117  pcmptcl  13121  pcprod  13125  fldivp1  13127  infpnlem2  13139  1arithlem4  13145  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemfrcn0  13273  ennnfonelemrn  13310  topnidg  13606  imasaddfnlemg  13635  imasaddflemg  13637  qusin  13647  mgmlrid  13699  mndass  13737  mhmco  13797  gzsumwcl  13802  gzsumwmhm  13803  grpass  13814  grpinvex  13815  dfgrp2  13832  grplid  13836  grprid  13837  grprcan  13842  grpinvssd  13882  grpinvval2  13888  mhmid  13918  mhmmnd  13919  ghmgrp  13921  mulgnn  13929  mulgnnp1  13933  mulgnegnn  13935  mulgnnsubcl  13937  mulgz  13953  issubg2m  13992  issubg4m  13996  subgintm  14001  nmzbi  14012  eqger  14027  eqgid  14029  eqgen  14030  qusgrp  14035  qusadd  14037  qusinv  14039  qussub  14040  ghminv  14053  ghmsub  14054  ghmrn  14060  resghm2b  14065  ghmf1  14076  conjsubg  14080  conjsubgen  14081  qusghm  14085  cmncom  14105  ablsubadd  14116  ablsubsub23  14129  ghmcmn  14131  gzsumreidx  14141  gsumsubmfi  14168  prdsidlem  14193  prdsinvlem  14196  pwselbasb  14206  pwsplusgval  14208  pwsmulrval  14209  pwsinvg  14215  mgpress  14230  srg1expzeq1  14299  ringinvnz1ne0  14354  ringinvnzdiv  14355  dvdsrd  14401  dvdsunit  14419  unitinvcl  14430  unitinvinv  14431  unitlinv  14433  unitrinv  14434  rhmunitinv  14485  subrngintm  14520  subrg1  14539  subrguss  14544  subrginv  14545  subrgunit  14547  subrgugrp  14548  subrgintm  14551  resrhm  14556  resrhm2b  14557  lmodass  14639  lmodlcan  14640  lmod0vlid  14655  lmod0vrid  14656  lmod0vid  14657  lmodvs0  14659  lcomf  14664  lmodvnegcl  14665  lmodvnegid  14666  lmodvsubadd  14675  lmodsubid  14684  lss1d  14720  lspval  14727  ellspsn6  14745  lspsnneg  14757  sralmod  14787  dflidl2rng  14818  lidlacl  14821  dflidl2  14825  df2idl2  14846  qusmul2  14866  quscrng  14870  cnfldmulg  14913  znf1o  14986  znidom  14992  aspval  15015  asclghm  15025  issubassa2  15035  psraddcl  15071  psr0lid  15073  tgss3  15179  clsval  15212  clsss3  15231  neiss2  15243  resttop  15271  resttopon2  15279  lmconst  15317  cnima  15321  cnntri  15325  cncnp  15331  cnrest  15336  cndis  15342  lmss  15347  lmff  15350  lmtopcnp  15351  txcnp  15372  upxp  15373  uptx  15375  cnmpt11  15384  hmeoima  15411  hmeoopn  15412  hmeocld  15413  hmeontr  15414  hmeoimaf1o  15415  mettri2  15463  met0  15465  metres2  15482  blpnf  15501  xblss2ps  15505  xblss2  15506  blbas  15534  blres  15535  xmetec  15538  mopnss  15551  xmstri2  15571  mstri2  15572  xmstri  15573  mstri  15574  xmstri3  15575  mstri3  15576  msrtri  15577  mopni3  15585  unimopn  15587  comet  15600  bdxmet  15602  climcncf  15685  dedekindeulemuub  15718  dedekindicclemuub  15727  ivthdichlem  15752  dvfgg  15789  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvfre  15811  dvmptfsum  15826  plyadd  15852  plymul  15853  reeff1olem  15872  reeff1o  15874  sinperlem  15909  abssinper  15947  reexplog  15972  relogexp  15973  cxpexpnn  15998  cxprec  16012  rpcxpmul2  16015  abscxp  16017  wilthlem1  16094  sgmval2  16098  sgmnncl  16102  0sgmppw  16107  perfectlem1  16113  lgsdir  16154  lgsprme0  16161  lgsdinn0  16167  gausslemma2dlem3  16182  gausslemma2dlem5a  16184  2lgslem1a2  16206  2lgslem1a  16207  2lgslem3  16220  2lgs  16223  umgredgprv  16356  umgrislfupgrdom  16372  uspgredgiedg  16419  uspgriedgedg  16420  usgrislfuspgrdom  16431  usgredg2en  16436  usgredgprv  16437  usgrpredgv  16439  usgredg  16441  usgrnloopv  16442  usgredgne  16445  usgredg3  16455  usgredgedg  16468  usgredgdomord  16471  usgr1vr  16489  subgruhgrfun  16509  subupgr  16514  subumgr  16515  subusgr  16516  umgrwlknloop  16609  wlkres  16620  clwwlkccatlem  16641  clwwlkccat  16642  depindlem1  16747  depindlem2  16748  depindlem3  16749  bj-inex  16933  bj-nn0suc  16990  bj-nn0sucALT  17004  trilpolemeq1  17089  trilpolemlt1  17090  trirec0  17093  nconstwlpolemgt0  17114