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  2121  csbiebt  3121  csbnestgf  3134  reuss2  3440  mpteq12  4113  otexg  4260  opelopabt  4293  sonr  4349  sotr  4350  issod  4351  so2nr  4353  so3nr  4354  ordelss  4411  onelon  4416  elrnmpt1s  4913  iota2  5245  funeu  5280  imadif  5335  fnbr  5357  feu  5437  f1ss  5466  f1ssres  5469  f1resf1  5470  dffo2  5481  foco  5488  foun  5520  fun11iun  5522  ffoss  5533  funbrfv  5596  fvco3  5629  fvopab6  5655  funfvbrb  5672  elpreima  5678  ffvelcdm  5692  ffvelcdmda  5694  dffo4  5707  fmptco  5725  fsn2  5733  fvconst2g  5773  fex  5788  funfvima  5791  f1elima  5817  f1ocnvfv1  5821  f1ocnvfv2  5822  cocan2  5832  foeqcnvco  5834  isocnv  5855  isores2  5857  isoini  5862  isoselem  5864  f1oiso  5870  f1ofveu  5907  eloprabga  6006  suppssof1  6150  ofco  6151  offveqb  6152  ofc1g  6153  ofc2g  6154  fnexALT  6165  f1dmex  6170  ot1stg  6207  ot2ndg  6208  ot3rdgg  6209  eqopi  6227  2ndrn  6238  fo2ndf  6282  smores3  6348  smores2  6349  smoel  6355  smoiso  6357  tfrlem1  6363  tfrlemisucaccv  6380  tfrlemibxssdm  6382  tfrlemiubacc  6385  tfr1onlemsucaccv  6396  tfr1onlembfn  6399  tfr1onlemubacc  6401  tfr1onlemaccex  6403  tfr1onlemres  6404  tfrcllemsucaccv  6409  tfrcllembfn  6412  tfrcllemubacc  6414  tfrcllemaccex  6416  tfrcllemres  6417  tfrcl  6419  frecrdg  6463  omv2  6520  nnasuc  6531  nnmsuc  6532  nnacom  6539  nnaass  6540  nnmass  6542  nntri1  6551  nndifsnid  6562  nnmordi  6571  swoer  6617  erth  6635  riinerm  6664  qliftlem  6669  ecovass  6700  ecoviass  6701  elmapssres  6729  fvixp  6759  f1domg  6814  endomtr  6846  xpsnen2g  6885  enen1  6898  enen2  6899  domen1  6900  domen2  6901  mapen  6904  mapxpen  6906  ssenen  6909  phplem1  6910  fidifsnid  6929  findcard  6946  findcard2  6947  findcard2s  6948  fieq0  7037  isotilem  7067  supisolem  7069  inflbti  7085  ordiso2  7096  djuex  7104  updjudhcoinlf  7141  updjudhcoinrg  7142  updjud  7143  ctssdccl  7172  enumctlemm  7175  nnnninf  7187  finomni  7201  pm54.43  7252  acfun  7269  ccfunen  7326  cc2lem  7328  cc3  7330  addclpi  7389  addasspig  7392  mulasspig  7394  addnidpig  7398  nnppipi  7405  ltanqi  7464  ltmnqi  7465  ltexnqq  7470  archnqq  7479  prarloclemarch2  7481  enq0sym  7494  enq0tr  7496  nqnq0pi  7500  nqnq0  7503  mulcanenq0ec  7507  addclnq0  7513  nqpnq0nq  7515  distrnq0  7521  addassnq0lemcl  7523  addassnq0  7524  prubl  7548  prarloclemlt  7555  genpdf  7570  genipv  7571  genpelvl  7574  genpelvu  7575  genpml  7579  genpmu  7580  genprndl  7583  genprndu  7584  genpassl  7586  genpassu  7587  genpassg  7588  addnqprl  7591  addnqpru  7592  addlocpr  7598  nqprm  7604  nqprl  7613  nqpru  7614  mulnqprl  7630  mulnqpru  7631  mullocprlem  7632  mullocpr  7633  addcomprg  7640  mulcomprg  7642  distrlem1prl  7644  distrlem1pru  7645  distrlem4prl  7646  distrlem4pru  7647  ltprordil  7651  1idprl  7652  1idpru  7653  ltpopr  7657  ltsopr  7658  ltaddpr  7659  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemfl  7671  ltexprlemrl  7672  ltexprlemfu  7673  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  prplnqu  7682  recexprlemloc  7693  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1l  7697  recexprlemss1u  7698  aptiprleml  7701  aptiprlemu  7702  cauappcvgprlemloc  7714  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemloc  7737  caucvgprlemladdrl  7740  caucvgprprlemml  7756  caucvgprprlemloc  7765  00sr  7831  map2psrprg  7867  suplocsrlempr  7869  suplocsrlem  7870  adddir  8012  axsuploc  8094  eqle  8113  le2tri3i  8130  mul4  8153  muladd11  8154  cnegexlem3  8198  addsub12  8234  2addsub  8235  addsubeq4  8236  subadd4  8265  negcon1  8273  negdi2  8279  negsubdi2  8280  neg2sub  8281  renegcl  8282  muladd  8405  subdir  8407  gt0ne0  8448  ltnegcon1  8484  lenegcon1  8487  eqord1  8504  eqord2  8505  recexre  8599  ltmul1  8613  recexap  8674  div12ap  8715  rerecapb  8864  p1le  8870  ltmul2  8877  gt0div  8891  ge0div  8892  zlem1lt  9376  nnaddm1cl  9381  zdceq  9395  gtndiv  9415  prime  9419  msqznn  9420  btwnz  9439  uzss  9616  eluzadd  9624  nn0pzuz  9655  supinfneg  9663  infsupneg  9664  divfnzn  9689  qnegcl  9704  qreccl  9710  elpqb  9718  xaddass  9938  xleadd1a  9942  xlesubadd  9952  elico2  10006  iccss  10010  iccsupr  10035  elfz5  10086  fznn  10158  difelfznle  10204  fzoaddel  10262  qdceq  10317  qbtwnxr  10329  flqbi2  10363  adddivflid  10364  fldivnn0  10367  divfl0  10368  flqmulnn0  10371  fldivnn0le  10375  fldiv4p1lem1div2  10377  ceiqle  10387  flqdiv  10395  modqmulnn  10416  frecuzrdgtcl  10486  frecuzrdgsuc  10488  frecuzrdgdomlem  10491  frecuzrdgfunlem  10493  frecuzrdgsuctlem  10497  seqm1g  10548  seq3caopr2  10567  seqcaopr2g  10568  iseqf1olemkle  10571  seq3f1olemp  10589  seqf1oglem2  10594  seqf1og  10595  seq3id  10599  seq3z  10602  expap0  10643  mulexp  10652  mulexpzap  10653  expmul  10658  leexp1a  10668  expubnd  10670  zesq  10732  bernneq  10734  bernneq3  10736  modqexp  10740  facdiv  10812  facndiv  10813  faclbnd3  10817  faclbnd6  10818  bccmpl  10828  bcpasc  10840  bccl  10841  seq3coll  10916  wrdsymb1  10953  shftlem  10963  ovshftex  10966  shftval4  10975  shftf  10977  shftcan2  10982  crim  11005  mulreap  11011  remul2  11020  immul2  11027  cjexp  11040  caucvgre  11128  r19.2uz  11140  sqrtsq2  11190  absnid  11220  absexp  11226  nn0abscl  11232  abslt  11235  lenegsq  11242  cau3lem  11261  minmax  11376  xrmaxadd  11407  clim  11427  climshftlemg  11448  climcn1  11454  climcn1lem  11465  clim2ser  11483  clim2ser2  11484  iserex  11485  isermulc2  11486  climub  11490  climcaucn  11497  serf0  11498  summodclem3  11526  summodclem2a  11527  summodclem2  11528  summodc  11529  fsum3  11533  fsumf1o  11536  fisumss  11538  isumss2  11539  fsumcl2lem  11544  fsumadd  11552  fsumsplit  11553  isummulc2  11572  fsum2d  11581  fsummulc2  11594  telfsumo  11612  fsumparts  11616  hash2iun1dif1  11626  bcxmas  11635  isumshft  11636  isumsplit  11637  expcnvap0  11648  geolim  11657  geolim2  11658  cvgratnnlemmn  11671  cvgratnnlemseq  11672  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  clim2divap  11686  prodmodclem3  11721  prodmodclem2a  11722  fprodseq  11729  fprodf1o  11734  fprodmul  11737  fprodsplitdc  11742  efcllemp  11804  reefcl  11814  efcj  11819  efaddlem  11820  efexp  11828  reeftlcl  11835  eftlub  11836  efsep  11837  effsumlt  11838  eflegeo  11847  retanclap  11868  demoivre  11919  demoivreALT  11920  eirraplem  11923  dvdsval3  11937  p1modz1  11940  iddvdsexp  11961  alzdvds  11999  addmodlteqALT  12004  nnehalf  12048  nno  12050  ndvdsadd  12075  divgcdnnr  12116  neggcd  12123  gcdabs  12128  bezoutlemmain  12138  bezoutlemaz  12143  bezoutlembz  12144  gcdmultiplez  12161  gcdzeq  12162  dvdssq  12171  nninfctlemfo  12180  algrf  12186  algcvg  12189  algcvga  12192  algfx  12193  eucalgf  12196  eucalgcvga  12199  neglcm  12216  lcmabs  12217  lcmdvds  12220  lcmgcdeq  12224  qredeq  12237  isprm3  12259  coprm  12285  prmrp  12286  isprm6  12288  prmdvdsexpb  12290  rpexp  12294  cncongrprm  12298  sqrt2irraplemnn  12320  phibndlem  12357  phiprmpw  12363  eulerthlemh  12372  eulerthlemth  12373  fermltl  12375  prmdivdiv  12378  modprm1div  12388  m1dvdsndvds  12389  coprimeprodsq  12398  pczpre  12438  pczcl  12439  pcexp  12450  pczdvds  12455  pczndvds  12457  pczndvds2  12459  pcdvdsb  12461  pcneg  12466  pcprmpw  12475  difsqpwdvds  12479  pcmptcl  12483  pcprod  12487  fldivp1  12489  infpnlem2  12501  1arithlem4  12507  ennnfonelemrn  12579  topnidg  12866  imasaddfnlemg  12900  imasaddflemg  12902  qusin  12912  mgmlrid  12965  mndass  13008  mhmco  13065  gsumsubm  13069  gsumwcl  13072  gsumwmhm  13073  grpass  13084  grpinvex  13085  dfgrp2  13102  grplid  13106  grprid  13107  grprcan  13112  grpinvssd  13152  grpinvval2  13158  mhmid  13188  mhmmnd  13189  ghmgrp  13191  mulgnn  13199  mulgnnp1  13203  mulgnegnn  13205  mulgnnsubcl  13207  mulgz  13223  issubg2m  13262  issubg4m  13266  subgintm  13271  nmzbi  13282  eqger  13297  eqgid  13299  eqgen  13300  qusgrp  13305  qusadd  13307  qusinv  13309  qussub  13310  ghminv  13323  ghmsub  13324  ghmrn  13330  resghm2b  13335  ghmf1  13346  conjsubg  13350  conjsubgen  13351  qusghm  13355  cmncom  13375  ablsubadd  13385  ablsubsub23  13398  ghmcmn  13400  gsumfzreidx  13410  mgpress  13430  srg1expzeq1  13494  ringinvnz1ne0  13548  ringinvnzdiv  13549  dvdsrd  13593  dvdsunit  13611  unitinvcl  13622  unitinvinv  13623  unitlinv  13625  unitrinv  13626  rhmunitinv  13677  subrngintm  13711  subrg1  13730  subrguss  13735  subrginv  13736  subrgunit  13738  subrgugrp  13739  subrgintm  13742  resrhm  13747  resrhm2b  13748  lmodass  13802  lmodlcan  13803  lmod0vlid  13817  lmod0vrid  13818  lmod0vid  13819  lmodvs0  13821  lcomf  13826  lmodvnegcl  13827  lmodvnegid  13828  lmodvsubadd  13837  lmodsubid  13846  lss1d  13882  lspval  13889  lspsnel6  13907  lspsnneg  13919  sralmod  13949  dflidl2rng  13980  lidlacl  13983  dflidl2  13987  df2idl2  14008  qusmul2  14028  quscrng  14032  cnfldmulg  14075  znf1o  14150  znidom  14156  psraddcl  14175  tgss3  14257  clsval  14290  clsss3  14309  neiss2  14321  resttop  14349  resttopon2  14357  lmconst  14395  cnima  14399  cnntri  14403  cncnp  14409  cnrest  14414  cndis  14420  lmss  14425  lmff  14428  lmtopcnp  14429  txcnp  14450  upxp  14451  uptx  14453  cnmpt11  14462  hmeoima  14489  hmeoopn  14490  hmeocld  14491  hmeontr  14492  hmeoimaf1o  14493  mettri2  14541  met0  14543  metres2  14560  blpnf  14579  xblss2ps  14583  xblss2  14584  blbas  14612  blres  14613  xmetec  14616  mopnss  14629  xmstri2  14649  mstri2  14650  xmstri  14651  mstri  14652  xmstri3  14653  mstri3  14654  msrtri  14655  mopni3  14663  unimopn  14665  comet  14678  bdxmet  14680  climcncf  14763  dedekindeulemuub  14796  dedekindicclemuub  14805  ivthdichlem  14830  dvfgg  14867  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvfre  14889  dvmptfsum  14904  plyadd  14930  plymul  14931  reeff1olem  14947  reeff1o  14949  sinperlem  14984  abssinper  15022  reexplog  15047  relogexp  15048  cxpexpnn  15072  cxprec  15086  abscxp  15090  wilthlem1  15153  lgsdir  15192  lgsprme0  15199  lgsdinn0  15205  gausslemma2dlem3  15220  gausslemma2dlem5a  15222  2lgslem1a2  15244  2lgslem1a  15245  2lgslem3  15258  2lgs  15261  bj-inex  15469  bj-nn0suc  15526  bj-nn0sucALT  15540  trilpolemeq1  15600  trilpolemlt1  15601  trirec0  15604  nconstwlpolemgt0  15624