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  941  3adantl1  1156  3adantl2  1157  3adantl3  1158  syl3anl1  1298  syl3anl3  1300  syl3anl  1301  stoic3  1451  eupick  2135  csbiebt  3141  csbnestgf  3154  reuss2  3461  mpteq12  4143  otexg  4292  opelopabt  4326  sonr  4382  sotr  4383  issod  4384  so2nr  4386  so3nr  4387  ordelss  4444  onelon  4449  elrnmpt1s  4947  iota2  5280  funeu  5315  imadif  5373  fnbr  5397  feu  5480  f1ss  5509  f1ssres  5512  f1resf1  5513  dffo2  5524  foco  5531  foun  5563  fun11iun  5565  ffoss  5576  funbrfv  5640  fvco3  5673  fvopab6  5699  funfvbrb  5716  elpreima  5722  ffvelcdm  5736  ffvelcdmda  5738  dffo4  5751  fmptco  5769  fsn2  5777  fvconst2g  5821  fex  5836  funfvima  5839  f1elima  5865  f1ocnvfv1  5869  f1ocnvfv2  5870  cocan2  5880  foeqcnvco  5882  isocnv  5903  isores2  5905  isoini  5910  isoselem  5912  f1oiso  5918  f1ofveu  5955  eloprabga  6055  suppssof1  6199  ofco  6200  offveqb  6201  ofc1g  6203  ofc2g  6204  caofid0l  6208  caofid0r  6209  caofid1  6210  caofid2  6211  fnexALT  6219  f1dmex  6224  ot1stg  6261  ot2ndg  6262  ot3rdgg  6263  eqopi  6281  2ndrn  6292  fo2ndf  6336  smores3  6402  smores2  6403  smoel  6409  smoiso  6411  tfrlem1  6417  tfrlemisucaccv  6434  tfrlemibxssdm  6436  tfrlemiubacc  6439  tfr1onlemsucaccv  6450  tfr1onlembfn  6453  tfr1onlemubacc  6455  tfr1onlemaccex  6457  tfr1onlemres  6458  tfrcllemsucaccv  6463  tfrcllembfn  6466  tfrcllemubacc  6468  tfrcllemaccex  6470  tfrcllemres  6471  tfrcl  6473  frecrdg  6517  omv2  6574  nnasuc  6585  nnmsuc  6586  nnacom  6593  nnaass  6594  nnmass  6596  nntri1  6605  nndifsnid  6616  nnmordi  6625  swoer  6671  erth  6689  riinerm  6718  qliftlem  6723  ecovass  6754  ecoviass  6755  elmapssres  6783  fvixp  6813  f1domg  6872  domssr  6892  endomtr  6905  xpsnen2g  6949  enen1  6962  enen2  6963  domen1  6964  domen2  6965  mapen  6968  mapxpen  6970  ssenen  6973  phplem1  6974  fidifsnid  6994  findcard  7011  findcard2  7012  findcard2s  7013  fieq0  7104  isotilem  7134  supisolem  7136  inflbti  7152  ordiso2  7163  djuex  7171  updjudhcoinlf  7208  updjudhcoinrg  7209  updjud  7210  ctssdccl  7239  enumctlemm  7242  nnnninf  7254  finomni  7268  pm54.43  7324  acfun  7350  ccfunen  7411  cc2lem  7413  cc3  7415  addclpi  7475  addasspig  7478  mulasspig  7480  addnidpig  7484  nnppipi  7491  ltanqi  7550  ltmnqi  7551  ltexnqq  7556  archnqq  7565  prarloclemarch2  7567  enq0sym  7580  enq0tr  7582  nqnq0pi  7586  nqnq0  7589  mulcanenq0ec  7593  addclnq0  7599  nqpnq0nq  7601  distrnq0  7607  addassnq0lemcl  7609  addassnq0  7610  prubl  7634  prarloclemlt  7641  genpdf  7656  genipv  7657  genpelvl  7660  genpelvu  7661  genpml  7665  genpmu  7666  genprndl  7669  genprndu  7670  genpassl  7672  genpassu  7673  genpassg  7674  addnqprl  7677  addnqpru  7678  addlocpr  7684  nqprm  7690  nqprl  7699  nqpru  7700  mulnqprl  7716  mulnqpru  7717  mullocprlem  7718  mullocpr  7719  addcomprg  7726  mulcomprg  7728  distrlem1prl  7730  distrlem1pru  7731  distrlem4prl  7732  distrlem4pru  7733  ltprordil  7737  1idprl  7738  1idpru  7739  ltpopr  7743  ltsopr  7744  ltaddpr  7745  ltexprlemm  7748  ltexprlemopl  7749  ltexprlemlol  7750  ltexprlemopu  7751  ltexprlemupu  7752  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemfl  7757  ltexprlemrl  7758  ltexprlemfu  7759  ltexprlemru  7760  addcanprleml  7762  addcanprlemu  7763  prplnqu  7768  recexprlemloc  7779  recexprlem1ssl  7781  recexprlem1ssu  7782  recexprlemss1l  7783  recexprlemss1u  7784  aptiprleml  7787  aptiprlemu  7788  cauappcvgprlemloc  7800  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprlemloc  7823  caucvgprlemladdrl  7826  caucvgprprlemml  7842  caucvgprprlemloc  7851  00sr  7917  map2psrprg  7953  suplocsrlempr  7955  suplocsrlem  7956  adddir  8098  axsuploc  8180  eqle  8199  le2tri3i  8216  mul4  8239  muladd11  8240  cnegexlem3  8284  addsub12  8320  2addsub  8321  addsubeq4  8322  subadd4  8351  negcon1  8359  negdi2  8365  negsubdi2  8366  neg2sub  8367  renegcl  8368  muladd  8491  subdir  8493  gt0ne0  8535  ltnegcon1  8571  lenegcon1  8574  eqord1  8591  eqord2  8592  recexre  8686  ltmul1  8700  recexap  8761  div12ap  8802  rerecapb  8951  p1le  8957  ltmul2  8964  gt0div  8978  ge0div  8979  zlem1lt  9464  nnaddm1cl  9469  zdceq  9483  gtndiv  9503  prime  9507  msqznn  9508  btwnz  9527  uzss  9704  eluzadd  9712  nn0pzuz  9743  supinfneg  9751  infsupneg  9752  divfnzn  9777  qnegcl  9792  qreccl  9798  elpqb  9806  xaddass  10026  xleadd1a  10030  xlesubadd  10040  elico2  10094  iccss  10098  iccsupr  10123  elfz5  10174  fznn  10246  difelfznle  10292  fzoaddel  10353  elincfzoext  10359  qdceq  10424  qbtwnxr  10437  flqbi2  10471  adddivflid  10472  fldivnn0  10475  divfl0  10476  flqmulnn0  10479  fldivnn0le  10483  fldiv4p1lem1div2  10485  ceiqle  10495  flqdiv  10503  modqmulnn  10524  frecuzrdgtcl  10594  frecuzrdgsuc  10596  frecuzrdgdomlem  10599  frecuzrdgfunlem  10601  frecuzrdgsuctlem  10605  seqm1g  10656  seq3caopr2  10675  seqcaopr2g  10676  iseqf1olemkle  10679  seq3f1olemp  10697  seqf1oglem2  10702  seqf1og  10703  seq3id  10707  seq3z  10710  expap0  10751  mulexp  10760  mulexpzap  10761  expmul  10766  leexp1a  10776  expubnd  10778  zesq  10840  bernneq  10842  bernneq3  10844  modqexp  10848  facdiv  10920  facndiv  10921  faclbnd3  10925  faclbnd6  10926  bccmpl  10936  bcpasc  10948  bccl  10949  seq3coll  11024  fundm2domnop  11028  wrdsymb1  11067  ccatfv0  11097  ccatrn  11103  ccat2s1cl  11125  lswccats1fst  11134  swrdspsleq  11158  pfxtrcfv  11184  pfxsuffeqwrdeq  11189  pfxlswccat  11204  wrdeqs1cat  11211  cats1un  11212  swrdccatin1  11216  pfxccatin12lem4  11217  swrdccatin2  11220  pfxccatin12  11224  swrdccat  11226  shftlem  11242  ovshftex  11245  shftval4  11254  shftf  11256  shftcan2  11261  crim  11284  mulreap  11290  remul2  11299  immul2  11306  cjexp  11319  caucvgre  11407  r19.2uz  11419  sqrtsq2  11469  absnid  11499  absexp  11505  nn0abscl  11511  abslt  11514  lenegsq  11521  cau3lem  11540  minmax  11656  xrmaxadd  11687  clim  11707  climshftlemg  11728  climcn1  11734  climcn1lem  11745  clim2ser  11763  clim2ser2  11764  iserex  11765  isermulc2  11766  climub  11770  climcaucn  11777  serf0  11778  summodclem3  11806  summodclem2a  11807  summodclem2  11808  summodc  11809  fsum3  11813  fsumf1o  11816  fisumss  11818  isumss2  11819  fsumcl2lem  11824  fsumadd  11832  fsumsplit  11833  isummulc2  11852  fsum2d  11861  fsummulc2  11874  telfsumo  11892  fsumparts  11896  hash2iun1dif1  11906  bcxmas  11915  isumshft  11916  isumsplit  11917  expcnvap0  11928  geolim  11937  geolim2  11938  cvgratnnlemmn  11951  cvgratnnlemseq  11952  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  clim2divap  11966  prodmodclem3  12001  prodmodclem2a  12002  fprodseq  12009  fprodf1o  12014  fprodmul  12017  fprodsplitdc  12022  efcllemp  12084  reefcl  12094  efcj  12099  efaddlem  12100  efexp  12108  reeftlcl  12115  eftlub  12116  efsep  12117  effsumlt  12118  eflegeo  12127  retanclap  12148  demoivre  12199  demoivreALT  12200  eirraplem  12203  dvdsval3  12217  p1modz1  12220  iddvdsexp  12241  alzdvds  12280  addmodlteqALT  12285  nnehalf  12330  nno  12332  ndvdsadd  12357  bitsp1e  12378  bitsp1o  12379  bitsinv1  12388  divgcdnnr  12412  neggcd  12419  gcdabs  12424  bezoutlemmain  12434  bezoutlemaz  12439  bezoutlembz  12440  gcdmultiplez  12457  gcdzeq  12458  dvdssq  12467  nninfctlemfo  12476  algrf  12482  algcvg  12485  algcvga  12488  algfx  12489  eucalgf  12492  eucalgcvga  12495  neglcm  12512  lcmabs  12513  lcmdvds  12516  lcmgcdeq  12520  qredeq  12533  isprm3  12555  coprm  12581  prmrp  12582  isprm6  12584  prmdvdsexpb  12586  rpexp  12590  cncongrprm  12594  sqrt2irraplemnn  12616  phibndlem  12653  phiprmpw  12659  eulerthlemh  12668  eulerthlemth  12669  fermltl  12671  prmdivdiv  12674  modprm1div  12685  m1dvdsndvds  12686  coprimeprodsq  12695  pczpre  12735  pczcl  12736  pcexp  12747  pczdvds  12752  pczndvds  12754  pczndvds2  12756  pcdvdsb  12758  pcneg  12763  pcprmpw  12772  difsqpwdvds  12776  pcmptcl  12780  pcprod  12784  fldivp1  12786  infpnlem2  12798  1arithlem4  12804  ennnfonelemrn  12905  topnidg  13199  pwselbasb  13240  pwsplusgval  13242  pwsmulrval  13243  imasaddfnlemg  13261  imasaddflemg  13263  qusin  13273  mgmlrid  13326  mndass  13371  prdsidlem  13394  mhmco  13437  gsumsubm  13441  gsumwcl  13444  gsumwmhm  13445  grpass  13456  grpinvex  13457  dfgrp2  13474  grplid  13478  grprid  13479  grprcan  13484  grpinvssd  13524  grpinvval2  13530  prdsinvlem  13555  pwsinvg  13559  mhmid  13566  mhmmnd  13567  ghmgrp  13569  mulgnn  13577  mulgnnp1  13581  mulgnegnn  13583  mulgnnsubcl  13585  mulgz  13601  issubg2m  13640  issubg4m  13644  subgintm  13649  nmzbi  13660  eqger  13675  eqgid  13677  eqgen  13678  qusgrp  13683  qusadd  13685  qusinv  13687  qussub  13688  ghminv  13701  ghmsub  13702  ghmrn  13708  resghm2b  13713  ghmf1  13724  conjsubg  13728  conjsubgen  13729  qusghm  13733  cmncom  13753  ablsubadd  13763  ablsubsub23  13776  ghmcmn  13778  gsumfzreidx  13788  mgpress  13808  srg1expzeq1  13872  ringinvnz1ne0  13926  ringinvnzdiv  13927  dvdsrd  13971  dvdsunit  13989  unitinvcl  14000  unitinvinv  14001  unitlinv  14003  unitrinv  14004  rhmunitinv  14055  subrngintm  14089  subrg1  14108  subrguss  14113  subrginv  14114  subrgunit  14116  subrgugrp  14117  subrgintm  14120  resrhm  14125  resrhm2b  14126  lmodass  14180  lmodlcan  14181  lmod0vlid  14195  lmod0vrid  14196  lmod0vid  14197  lmodvs0  14199  lcomf  14204  lmodvnegcl  14205  lmodvnegid  14206  lmodvsubadd  14215  lmodsubid  14224  lss1d  14260  lspval  14267  lspsnel6  14285  lspsnneg  14297  sralmod  14327  dflidl2rng  14358  lidlacl  14361  dflidl2  14365  df2idl2  14386  qusmul2  14406  quscrng  14410  cnfldmulg  14453  znf1o  14528  znidom  14534  psraddcl  14557  psr0lid  14559  tgss3  14665  clsval  14698  clsss3  14717  neiss2  14729  resttop  14757  resttopon2  14765  lmconst  14803  cnima  14807  cnntri  14811  cncnp  14817  cnrest  14822  cndis  14828  lmss  14833  lmff  14836  lmtopcnp  14837  txcnp  14858  upxp  14859  uptx  14861  cnmpt11  14870  hmeoima  14897  hmeoopn  14898  hmeocld  14899  hmeontr  14900  hmeoimaf1o  14901  mettri2  14949  met0  14951  metres2  14968  blpnf  14987  xblss2ps  14991  xblss2  14992  blbas  15020  blres  15021  xmetec  15024  mopnss  15037  xmstri2  15057  mstri2  15058  xmstri  15059  mstri  15060  xmstri3  15061  mstri3  15062  msrtri  15063  mopni3  15071  unimopn  15073  comet  15086  bdxmet  15088  climcncf  15171  dedekindeulemuub  15204  dedekindicclemuub  15213  ivthdichlem  15238  dvfgg  15275  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvfre  15297  dvmptfsum  15312  plyadd  15338  plymul  15339  reeff1olem  15358  reeff1o  15360  sinperlem  15395  abssinper  15433  reexplog  15458  relogexp  15459  cxpexpnn  15483  cxprec  15497  rpcxpmul2  15500  abscxp  15502  wilthlem1  15567  sgmval2  15571  sgmnncl  15575  0sgmppw  15580  perfectlem1  15586  lgsdir  15627  lgsprme0  15634  lgsdinn0  15640  gausslemma2dlem3  15655  gausslemma2dlem5a  15657  2lgslem1a2  15679  2lgslem1a  15680  2lgslem3  15693  2lgs  15696  umgrislfupgrdom  15837  bj-inex  16042  bj-nn0suc  16099  bj-nn0sucALT  16113  trilpolemeq1  16181  trilpolemlt1  16182  trirec0  16185  nconstwlpolemgt0  16205