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  3443  mpteq12  4116  otexg  4263  opelopabt  4296  sonr  4352  sotr  4353  issod  4354  so2nr  4356  so3nr  4357  ordelss  4414  onelon  4419  elrnmpt1s  4916  iota2  5248  funeu  5283  imadif  5338  fnbr  5360  feu  5440  f1ss  5469  f1ssres  5472  f1resf1  5473  dffo2  5484  foco  5491  foun  5523  fun11iun  5525  ffoss  5536  funbrfv  5599  fvco3  5632  fvopab6  5658  funfvbrb  5675  elpreima  5681  ffvelcdm  5695  ffvelcdmda  5697  dffo4  5710  fmptco  5728  fsn2  5736  fvconst2g  5776  fex  5791  funfvima  5794  f1elima  5820  f1ocnvfv1  5824  f1ocnvfv2  5825  cocan2  5835  foeqcnvco  5837  isocnv  5858  isores2  5860  isoini  5865  isoselem  5867  f1oiso  5873  f1ofveu  5910  eloprabga  6009  suppssof1  6153  ofco  6154  offveqb  6155  ofc1g  6156  ofc2g  6157  fnexALT  6168  f1dmex  6173  ot1stg  6210  ot2ndg  6211  ot3rdgg  6212  eqopi  6230  2ndrn  6241  fo2ndf  6285  smores3  6351  smores2  6352  smoel  6358  smoiso  6360  tfrlem1  6366  tfrlemisucaccv  6383  tfrlemibxssdm  6385  tfrlemiubacc  6388  tfr1onlemsucaccv  6399  tfr1onlembfn  6402  tfr1onlemubacc  6404  tfr1onlemaccex  6406  tfr1onlemres  6407  tfrcllemsucaccv  6412  tfrcllembfn  6415  tfrcllemubacc  6417  tfrcllemaccex  6419  tfrcllemres  6420  tfrcl  6422  frecrdg  6466  omv2  6523  nnasuc  6534  nnmsuc  6535  nnacom  6542  nnaass  6543  nnmass  6545  nntri1  6554  nndifsnid  6565  nnmordi  6574  swoer  6620  erth  6638  riinerm  6667  qliftlem  6672  ecovass  6703  ecoviass  6704  elmapssres  6732  fvixp  6762  f1domg  6817  endomtr  6849  xpsnen2g  6888  enen1  6901  enen2  6902  domen1  6903  domen2  6904  mapen  6907  mapxpen  6909  ssenen  6912  phplem1  6913  fidifsnid  6932  findcard  6949  findcard2  6950  findcard2s  6951  fieq0  7042  isotilem  7072  supisolem  7074  inflbti  7090  ordiso2  7101  djuex  7109  updjudhcoinlf  7146  updjudhcoinrg  7147  updjud  7148  ctssdccl  7177  enumctlemm  7180  nnnninf  7192  finomni  7206  pm54.43  7257  acfun  7274  ccfunen  7331  cc2lem  7333  cc3  7335  addclpi  7394  addasspig  7397  mulasspig  7399  addnidpig  7403  nnppipi  7410  ltanqi  7469  ltmnqi  7470  ltexnqq  7475  archnqq  7484  prarloclemarch2  7486  enq0sym  7499  enq0tr  7501  nqnq0pi  7505  nqnq0  7508  mulcanenq0ec  7512  addclnq0  7518  nqpnq0nq  7520  distrnq0  7526  addassnq0lemcl  7528  addassnq0  7529  prubl  7553  prarloclemlt  7560  genpdf  7575  genipv  7576  genpelvl  7579  genpelvu  7580  genpml  7584  genpmu  7585  genprndl  7588  genprndu  7589  genpassl  7591  genpassu  7592  genpassg  7593  addnqprl  7596  addnqpru  7597  addlocpr  7603  nqprm  7609  nqprl  7618  nqpru  7619  mulnqprl  7635  mulnqpru  7636  mullocprlem  7637  mullocpr  7638  addcomprg  7645  mulcomprg  7647  distrlem1prl  7649  distrlem1pru  7650  distrlem4prl  7651  distrlem4pru  7652  ltprordil  7656  1idprl  7657  1idpru  7658  ltpopr  7662  ltsopr  7663  ltaddpr  7664  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  prplnqu  7687  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1l  7702  recexprlemss1u  7703  aptiprleml  7706  aptiprlemu  7707  cauappcvgprlemloc  7719  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemloc  7742  caucvgprlemladdrl  7745  caucvgprprlemml  7761  caucvgprprlemloc  7770  00sr  7836  map2psrprg  7872  suplocsrlempr  7874  suplocsrlem  7875  adddir  8017  axsuploc  8099  eqle  8118  le2tri3i  8135  mul4  8158  muladd11  8159  cnegexlem3  8203  addsub12  8239  2addsub  8240  addsubeq4  8241  subadd4  8270  negcon1  8278  negdi2  8284  negsubdi2  8285  neg2sub  8286  renegcl  8287  muladd  8410  subdir  8412  gt0ne0  8454  ltnegcon1  8490  lenegcon1  8493  eqord1  8510  eqord2  8511  recexre  8605  ltmul1  8619  recexap  8680  div12ap  8721  rerecapb  8870  p1le  8876  ltmul2  8883  gt0div  8897  ge0div  8898  zlem1lt  9382  nnaddm1cl  9387  zdceq  9401  gtndiv  9421  prime  9425  msqznn  9426  btwnz  9445  uzss  9622  eluzadd  9630  nn0pzuz  9661  supinfneg  9669  infsupneg  9670  divfnzn  9695  qnegcl  9710  qreccl  9716  elpqb  9724  xaddass  9944  xleadd1a  9948  xlesubadd  9958  elico2  10012  iccss  10016  iccsupr  10041  elfz5  10092  fznn  10164  difelfznle  10210  fzoaddel  10268  qdceq  10334  qbtwnxr  10347  flqbi2  10381  adddivflid  10382  fldivnn0  10385  divfl0  10386  flqmulnn0  10389  fldivnn0le  10393  fldiv4p1lem1div2  10395  ceiqle  10405  flqdiv  10413  modqmulnn  10434  frecuzrdgtcl  10504  frecuzrdgsuc  10506  frecuzrdgdomlem  10509  frecuzrdgfunlem  10511  frecuzrdgsuctlem  10515  seqm1g  10566  seq3caopr2  10585  seqcaopr2g  10586  iseqf1olemkle  10589  seq3f1olemp  10607  seqf1oglem2  10612  seqf1og  10613  seq3id  10617  seq3z  10620  expap0  10661  mulexp  10670  mulexpzap  10671  expmul  10676  leexp1a  10686  expubnd  10688  zesq  10750  bernneq  10752  bernneq3  10754  modqexp  10758  facdiv  10830  facndiv  10831  faclbnd3  10835  faclbnd6  10836  bccmpl  10846  bcpasc  10858  bccl  10859  seq3coll  10934  wrdsymb1  10971  shftlem  10981  ovshftex  10984  shftval4  10993  shftf  10995  shftcan2  11000  crim  11023  mulreap  11029  remul2  11038  immul2  11045  cjexp  11058  caucvgre  11146  r19.2uz  11158  sqrtsq2  11208  absnid  11238  absexp  11244  nn0abscl  11250  abslt  11253  lenegsq  11260  cau3lem  11279  minmax  11395  xrmaxadd  11426  clim  11446  climshftlemg  11467  climcn1  11473  climcn1lem  11484  clim2ser  11502  clim2ser2  11503  iserex  11504  isermulc2  11505  climub  11509  climcaucn  11516  serf0  11517  summodclem3  11545  summodclem2a  11546  summodclem2  11547  summodc  11548  fsum3  11552  fsumf1o  11555  fisumss  11557  isumss2  11558  fsumcl2lem  11563  fsumadd  11571  fsumsplit  11572  isummulc2  11591  fsum2d  11600  fsummulc2  11613  telfsumo  11631  fsumparts  11635  hash2iun1dif1  11645  bcxmas  11654  isumshft  11655  isumsplit  11656  expcnvap0  11667  geolim  11676  geolim2  11677  cvgratnnlemmn  11690  cvgratnnlemseq  11691  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  clim2divap  11705  prodmodclem3  11740  prodmodclem2a  11741  fprodseq  11748  fprodf1o  11753  fprodmul  11756  fprodsplitdc  11761  efcllemp  11823  reefcl  11833  efcj  11838  efaddlem  11839  efexp  11847  reeftlcl  11854  eftlub  11855  efsep  11856  effsumlt  11857  eflegeo  11866  retanclap  11887  demoivre  11938  demoivreALT  11939  eirraplem  11942  dvdsval3  11956  p1modz1  11959  iddvdsexp  11980  alzdvds  12019  addmodlteqALT  12024  nnehalf  12069  nno  12071  ndvdsadd  12096  bitsp1e  12116  bitsp1o  12117  divgcdnnr  12143  neggcd  12150  gcdabs  12155  bezoutlemmain  12165  bezoutlemaz  12170  bezoutlembz  12171  gcdmultiplez  12188  gcdzeq  12189  dvdssq  12198  nninfctlemfo  12207  algrf  12213  algcvg  12216  algcvga  12219  algfx  12220  eucalgf  12223  eucalgcvga  12226  neglcm  12243  lcmabs  12244  lcmdvds  12247  lcmgcdeq  12251  qredeq  12264  isprm3  12286  coprm  12312  prmrp  12313  isprm6  12315  prmdvdsexpb  12317  rpexp  12321  cncongrprm  12325  sqrt2irraplemnn  12347  phibndlem  12384  phiprmpw  12390  eulerthlemh  12399  eulerthlemth  12400  fermltl  12402  prmdivdiv  12405  modprm1div  12416  m1dvdsndvds  12417  coprimeprodsq  12426  pczpre  12466  pczcl  12467  pcexp  12478  pczdvds  12483  pczndvds  12485  pczndvds2  12487  pcdvdsb  12489  pcneg  12494  pcprmpw  12503  difsqpwdvds  12507  pcmptcl  12511  pcprod  12515  fldivp1  12517  infpnlem2  12529  1arithlem4  12535  ennnfonelemrn  12636  topnidg  12923  imasaddfnlemg  12957  imasaddflemg  12959  qusin  12969  mgmlrid  13022  mndass  13065  mhmco  13122  gsumsubm  13126  gsumwcl  13129  gsumwmhm  13130  grpass  13141  grpinvex  13142  dfgrp2  13159  grplid  13163  grprid  13164  grprcan  13169  grpinvssd  13209  grpinvval2  13215  mhmid  13245  mhmmnd  13246  ghmgrp  13248  mulgnn  13256  mulgnnp1  13260  mulgnegnn  13262  mulgnnsubcl  13264  mulgz  13280  issubg2m  13319  issubg4m  13323  subgintm  13328  nmzbi  13339  eqger  13354  eqgid  13356  eqgen  13357  qusgrp  13362  qusadd  13364  qusinv  13366  qussub  13367  ghminv  13380  ghmsub  13381  ghmrn  13387  resghm2b  13392  ghmf1  13403  conjsubg  13407  conjsubgen  13408  qusghm  13412  cmncom  13432  ablsubadd  13442  ablsubsub23  13455  ghmcmn  13457  gsumfzreidx  13467  mgpress  13487  srg1expzeq1  13551  ringinvnz1ne0  13605  ringinvnzdiv  13606  dvdsrd  13650  dvdsunit  13668  unitinvcl  13679  unitinvinv  13680  unitlinv  13682  unitrinv  13683  rhmunitinv  13734  subrngintm  13768  subrg1  13787  subrguss  13792  subrginv  13793  subrgunit  13795  subrgugrp  13796  subrgintm  13799  resrhm  13804  resrhm2b  13805  lmodass  13859  lmodlcan  13860  lmod0vlid  13874  lmod0vrid  13875  lmod0vid  13876  lmodvs0  13878  lcomf  13883  lmodvnegcl  13884  lmodvnegid  13885  lmodvsubadd  13894  lmodsubid  13903  lss1d  13939  lspval  13946  lspsnel6  13964  lspsnneg  13976  sralmod  14006  dflidl2rng  14037  lidlacl  14040  dflidl2  14044  df2idl2  14065  qusmul2  14085  quscrng  14089  cnfldmulg  14132  znf1o  14207  znidom  14213  psraddcl  14232  tgss3  14314  clsval  14347  clsss3  14366  neiss2  14378  resttop  14406  resttopon2  14414  lmconst  14452  cnima  14456  cnntri  14460  cncnp  14466  cnrest  14471  cndis  14477  lmss  14482  lmff  14485  lmtopcnp  14486  txcnp  14507  upxp  14508  uptx  14510  cnmpt11  14519  hmeoima  14546  hmeoopn  14547  hmeocld  14548  hmeontr  14549  hmeoimaf1o  14550  mettri2  14598  met0  14600  metres2  14617  blpnf  14636  xblss2ps  14640  xblss2  14641  blbas  14669  blres  14670  xmetec  14673  mopnss  14686  xmstri2  14706  mstri2  14707  xmstri  14708  mstri  14709  xmstri3  14710  mstri3  14711  msrtri  14712  mopni3  14720  unimopn  14722  comet  14735  bdxmet  14737  climcncf  14820  dedekindeulemuub  14853  dedekindicclemuub  14862  ivthdichlem  14887  dvfgg  14924  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvfre  14946  dvmptfsum  14961  plyadd  14987  plymul  14988  reeff1olem  15007  reeff1o  15009  sinperlem  15044  abssinper  15082  reexplog  15107  relogexp  15108  cxpexpnn  15132  cxprec  15146  rpcxpmul2  15149  abscxp  15151  wilthlem1  15216  sgmval2  15220  sgmnncl  15224  0sgmppw  15229  perfectlem1  15235  lgsdir  15276  lgsprme0  15283  lgsdinn0  15289  gausslemma2dlem3  15304  gausslemma2dlem5a  15306  2lgslem1a2  15328  2lgslem1a  15329  2lgslem3  15342  2lgs  15345  bj-inex  15553  bj-nn0suc  15610  bj-nn0sucALT  15624  trilpolemeq1  15684  trilpolemlt1  15685  trirec0  15688  nconstwlpolemgt0  15708