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  944  dfifp2dc  987  3adantl1  1177  3adantl2  1178  3adantl3  1179  syl3anl1  1319  syl3anl3  1321  syl3anl  1322  stoic3  1473  eupick  2157  csbiebt  3164  csbnestgf  3177  reuss2  3484  mpteq12  4166  otexg  4315  opelopabt  4349  sonr  4407  sotr  4408  issod  4409  so2nr  4411  so3nr  4412  ordelss  4469  onelon  4474  elrnmpt1s  4973  iota2  5307  funeu  5342  imadif  5400  fnbr  5424  feu  5507  f1ss  5536  f1ssres  5539  f1resf1  5540  dffo2  5551  foco  5558  foun  5590  fun11iun  5592  ffoss  5603  funbrfv  5669  fvco3  5704  fvopab6  5730  funfvbrb  5747  elpreima  5753  ffvelcdm  5767  ffvelcdmda  5769  dffo4  5782  fmptco  5800  fsn2  5808  fvconst2g  5852  fex  5867  funfvima  5870  f1elima  5896  f1ocnvfv1  5900  f1ocnvfv2  5901  cocan2  5911  foeqcnvco  5913  isocnv  5934  isores2  5936  isoini  5941  isoselem  5943  f1oiso  5949  f1ofveu  5988  eloprabga  6090  suppssof1  6234  ofco  6235  offveqb  6236  ofc1g  6238  ofc2g  6239  caofid0l  6243  caofid0r  6244  caofid1  6245  caofid2  6246  fnexALT  6254  f1dmex  6259  ot1stg  6296  ot2ndg  6297  ot3rdgg  6298  eqopi  6316  2ndrn  6327  fo2ndf  6371  smores3  6437  smores2  6438  smoel  6444  smoiso  6446  tfrlem1  6452  tfrlemisucaccv  6469  tfrlemibxssdm  6471  tfrlemiubacc  6474  tfr1onlemsucaccv  6485  tfr1onlembfn  6488  tfr1onlemubacc  6490  tfr1onlemaccex  6492  tfr1onlemres  6493  tfrcllemsucaccv  6498  tfrcllembfn  6501  tfrcllemubacc  6503  tfrcllemaccex  6505  tfrcllemres  6506  tfrcl  6508  frecrdg  6552  omv2  6609  nnasuc  6620  nnmsuc  6621  nnacom  6628  nnaass  6629  nnmass  6631  nntri1  6640  nndifsnid  6651  nnmordi  6660  swoer  6706  erth  6724  riinerm  6753  qliftlem  6758  ecovass  6789  ecoviass  6790  elmapssres  6818  fvixp  6848  f1domg  6907  domssr  6927  endomtr  6940  xpsnen2g  6984  enen1  6997  enen2  6998  domen1  6999  domen2  7000  mapen  7003  mapxpen  7005  ssenen  7008  phplem1  7009  fidifsnid  7029  findcard  7046  findcard2  7047  findcard2s  7048  fieq0  7139  isotilem  7169  supisolem  7171  inflbti  7187  ordiso2  7198  djuex  7206  updjudhcoinlf  7243  updjudhcoinrg  7244  updjud  7245  ctssdccl  7274  enumctlemm  7277  nnnninf  7289  finomni  7303  pm54.43  7359  acfun  7385  ccfunen  7446  cc2lem  7448  cc3  7450  addclpi  7510  addasspig  7513  mulasspig  7515  addnidpig  7519  nnppipi  7526  ltanqi  7585  ltmnqi  7586  ltexnqq  7591  archnqq  7600  prarloclemarch2  7602  enq0sym  7615  enq0tr  7617  nqnq0pi  7621  nqnq0  7624  mulcanenq0ec  7628  addclnq0  7634  nqpnq0nq  7636  distrnq0  7642  addassnq0lemcl  7644  addassnq0  7645  prubl  7669  prarloclemlt  7676  genpdf  7691  genipv  7692  genpelvl  7695  genpelvu  7696  genpml  7700  genpmu  7701  genprndl  7704  genprndu  7705  genpassl  7707  genpassu  7708  genpassg  7709  addnqprl  7712  addnqpru  7713  addlocpr  7719  nqprm  7725  nqprl  7734  nqpru  7735  mulnqprl  7751  mulnqpru  7752  mullocprlem  7753  mullocpr  7754  addcomprg  7761  mulcomprg  7763  distrlem1prl  7765  distrlem1pru  7766  distrlem4prl  7767  distrlem4pru  7768  ltprordil  7772  1idprl  7773  1idpru  7774  ltpopr  7778  ltsopr  7779  ltaddpr  7780  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  ltexprlemdisj  7789  ltexprlemloc  7790  ltexprlemfl  7792  ltexprlemrl  7793  ltexprlemfu  7794  ltexprlemru  7795  addcanprleml  7797  addcanprlemu  7798  prplnqu  7803  recexprlemloc  7814  recexprlem1ssl  7816  recexprlem1ssu  7817  recexprlemss1l  7818  recexprlemss1u  7819  aptiprleml  7822  aptiprlemu  7823  cauappcvgprlemloc  7835  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemloc  7858  caucvgprlemladdrl  7861  caucvgprprlemml  7877  caucvgprprlemloc  7886  00sr  7952  map2psrprg  7988  suplocsrlempr  7990  suplocsrlem  7991  adddir  8133  axsuploc  8215  eqle  8234  le2tri3i  8251  mul4  8274  muladd11  8275  cnegexlem3  8319  addsub12  8355  2addsub  8356  addsubeq4  8357  subadd4  8386  negcon1  8394  negdi2  8400  negsubdi2  8401  neg2sub  8402  renegcl  8403  muladd  8526  subdir  8528  gt0ne0  8570  ltnegcon1  8606  lenegcon1  8609  eqord1  8626  eqord2  8627  recexre  8721  ltmul1  8735  recexap  8796  div12ap  8837  rerecapb  8986  p1le  8992  ltmul2  8999  gt0div  9013  ge0div  9014  zlem1lt  9499  nnaddm1cl  9504  zdceq  9518  gtndiv  9538  prime  9542  msqznn  9543  btwnz  9562  uzss  9739  eluzadd  9747  nn0pzuz  9778  supinfneg  9786  infsupneg  9787  divfnzn  9812  qnegcl  9827  qreccl  9833  elpqb  9841  xaddass  10061  xleadd1a  10065  xlesubadd  10075  elico2  10129  iccss  10133  iccsupr  10158  elfz5  10209  fznn  10281  difelfznle  10327  fzoaddel  10388  elincfzoext  10394  qdceq  10459  qbtwnxr  10472  flqbi2  10506  adddivflid  10507  fldivnn0  10510  divfl0  10511  flqmulnn0  10514  fldivnn0le  10518  fldiv4p1lem1div2  10520  ceiqle  10530  flqdiv  10538  modqmulnn  10559  frecuzrdgtcl  10629  frecuzrdgsuc  10631  frecuzrdgdomlem  10634  frecuzrdgfunlem  10636  frecuzrdgsuctlem  10640  seqm1g  10691  seq3caopr2  10710  seqcaopr2g  10711  iseqf1olemkle  10714  seq3f1olemp  10732  seqf1oglem2  10737  seqf1og  10738  seq3id  10742  seq3z  10745  expap0  10786  mulexp  10795  mulexpzap  10796  expmul  10801  leexp1a  10811  expubnd  10813  zesq  10875  bernneq  10877  bernneq3  10879  modqexp  10883  facdiv  10955  facndiv  10956  faclbnd3  10960  faclbnd6  10961  bccmpl  10971  bcpasc  10983  bccl  10984  seq3coll  11059  fundm2domnop  11063  wrdsymb1  11103  ccatfv0  11133  ccatrn  11139  ccat2s1cl  11161  lswccats1fst  11170  swrdspsleq  11194  pfxtrcfv  11220  pfxsuffeqwrdeq  11225  pfxlswccat  11240  wrdeqs1cat  11247  cats1un  11248  swrdccatin1  11252  pfxccatin12lem4  11253  swrdccatin2  11256  pfxccatin12  11260  swrdccat  11262  shftlem  11322  ovshftex  11325  shftval4  11334  shftf  11336  shftcan2  11341  crim  11364  mulreap  11370  remul2  11379  immul2  11386  cjexp  11399  caucvgre  11487  r19.2uz  11499  sqrtsq2  11549  absnid  11579  absexp  11585  nn0abscl  11591  abslt  11594  lenegsq  11601  cau3lem  11620  minmax  11736  xrmaxadd  11767  clim  11787  climshftlemg  11808  climcn1  11814  climcn1lem  11825  clim2ser  11843  clim2ser2  11844  iserex  11845  isermulc2  11846  climub  11850  climcaucn  11857  serf0  11858  summodclem3  11886  summodclem2a  11887  summodclem2  11888  summodc  11889  fsum3  11893  fsumf1o  11896  fisumss  11898  isumss2  11899  fsumcl2lem  11904  fsumadd  11912  fsumsplit  11913  isummulc2  11932  fsum2d  11941  fsummulc2  11954  telfsumo  11972  fsumparts  11976  hash2iun1dif1  11986  bcxmas  11995  isumshft  11996  isumsplit  11997  expcnvap0  12008  geolim  12017  geolim2  12018  cvgratnnlemmn  12031  cvgratnnlemseq  12032  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  clim2divap  12046  prodmodclem3  12081  prodmodclem2a  12082  fprodseq  12089  fprodf1o  12094  fprodmul  12097  fprodsplitdc  12102  efcllemp  12164  reefcl  12174  efcj  12179  efaddlem  12180  efexp  12188  reeftlcl  12195  eftlub  12196  efsep  12197  effsumlt  12198  eflegeo  12207  retanclap  12228  demoivre  12279  demoivreALT  12280  eirraplem  12283  dvdsval3  12297  p1modz1  12300  iddvdsexp  12321  alzdvds  12360  addmodlteqALT  12365  nnehalf  12410  nno  12412  ndvdsadd  12437  bitsp1e  12458  bitsp1o  12459  bitsinv1  12468  divgcdnnr  12492  neggcd  12499  gcdabs  12504  bezoutlemmain  12514  bezoutlemaz  12519  bezoutlembz  12520  gcdmultiplez  12537  gcdzeq  12538  dvdssq  12547  nninfctlemfo  12556  algrf  12562  algcvg  12565  algcvga  12568  algfx  12569  eucalgf  12572  eucalgcvga  12575  neglcm  12592  lcmabs  12593  lcmdvds  12596  lcmgcdeq  12600  qredeq  12613  isprm3  12635  coprm  12661  prmrp  12662  isprm6  12664  prmdvdsexpb  12666  rpexp  12670  cncongrprm  12674  sqrt2irraplemnn  12696  phibndlem  12733  phiprmpw  12739  eulerthlemh  12748  eulerthlemth  12749  fermltl  12751  prmdivdiv  12754  modprm1div  12765  m1dvdsndvds  12766  coprimeprodsq  12775  pczpre  12815  pczcl  12816  pcexp  12827  pczdvds  12832  pczndvds  12834  pczndvds2  12836  pcdvdsb  12838  pcneg  12843  pcprmpw  12852  difsqpwdvds  12856  pcmptcl  12860  pcprod  12864  fldivp1  12866  infpnlem2  12878  1arithlem4  12884  ennnfonelemrn  12985  topnidg  13280  pwselbasb  13321  pwsplusgval  13323  pwsmulrval  13324  imasaddfnlemg  13342  imasaddflemg  13344  qusin  13354  mgmlrid  13407  mndass  13452  prdsidlem  13475  mhmco  13518  gsumsubm  13522  gsumwcl  13525  gsumwmhm  13526  grpass  13537  grpinvex  13538  dfgrp2  13555  grplid  13559  grprid  13560  grprcan  13565  grpinvssd  13605  grpinvval2  13611  prdsinvlem  13636  pwsinvg  13640  mhmid  13647  mhmmnd  13648  ghmgrp  13650  mulgnn  13658  mulgnnp1  13662  mulgnegnn  13664  mulgnnsubcl  13666  mulgz  13682  issubg2m  13721  issubg4m  13725  subgintm  13730  nmzbi  13741  eqger  13756  eqgid  13758  eqgen  13759  qusgrp  13764  qusadd  13766  qusinv  13768  qussub  13769  ghminv  13782  ghmsub  13783  ghmrn  13789  resghm2b  13794  ghmf1  13805  conjsubg  13809  conjsubgen  13810  qusghm  13814  cmncom  13834  ablsubadd  13844  ablsubsub23  13857  ghmcmn  13859  gsumfzreidx  13869  mgpress  13889  srg1expzeq1  13953  ringinvnz1ne0  14007  ringinvnzdiv  14008  dvdsrd  14052  dvdsunit  14070  unitinvcl  14081  unitinvinv  14082  unitlinv  14084  unitrinv  14085  rhmunitinv  14136  subrngintm  14170  subrg1  14189  subrguss  14194  subrginv  14195  subrgunit  14197  subrgugrp  14198  subrgintm  14201  resrhm  14206  resrhm2b  14207  lmodass  14261  lmodlcan  14262  lmod0vlid  14276  lmod0vrid  14277  lmod0vid  14278  lmodvs0  14280  lcomf  14285  lmodvnegcl  14286  lmodvnegid  14287  lmodvsubadd  14296  lmodsubid  14305  lss1d  14341  lspval  14348  lspsnel6  14366  lspsnneg  14378  sralmod  14408  dflidl2rng  14439  lidlacl  14442  dflidl2  14446  df2idl2  14467  qusmul2  14487  quscrng  14491  cnfldmulg  14534  znf1o  14609  znidom  14615  psraddcl  14638  psr0lid  14640  tgss3  14746  clsval  14779  clsss3  14798  neiss2  14810  resttop  14838  resttopon2  14846  lmconst  14884  cnima  14888  cnntri  14892  cncnp  14898  cnrest  14903  cndis  14909  lmss  14914  lmff  14917  lmtopcnp  14918  txcnp  14939  upxp  14940  uptx  14942  cnmpt11  14951  hmeoima  14978  hmeoopn  14979  hmeocld  14980  hmeontr  14981  hmeoimaf1o  14982  mettri2  15030  met0  15032  metres2  15049  blpnf  15068  xblss2ps  15072  xblss2  15073  blbas  15101  blres  15102  xmetec  15105  mopnss  15118  xmstri2  15138  mstri2  15139  xmstri  15140  mstri  15141  xmstri3  15142  mstri3  15143  msrtri  15144  mopni3  15152  unimopn  15154  comet  15167  bdxmet  15169  climcncf  15252  dedekindeulemuub  15285  dedekindicclemuub  15294  ivthdichlem  15319  dvfgg  15356  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvfre  15378  dvmptfsum  15393  plyadd  15419  plymul  15420  reeff1olem  15439  reeff1o  15441  sinperlem  15476  abssinper  15514  reexplog  15539  relogexp  15540  cxpexpnn  15564  cxprec  15578  rpcxpmul2  15581  abscxp  15583  wilthlem1  15648  sgmval2  15652  sgmnncl  15656  0sgmppw  15661  perfectlem1  15667  lgsdir  15708  lgsprme0  15715  lgsdinn0  15721  gausslemma2dlem3  15736  gausslemma2dlem5a  15738  2lgslem1a2  15760  2lgslem1a  15761  2lgslem3  15774  2lgs  15777  umgredgprv  15909  umgrislfupgrdom  15923  uspgredgiedg  15970  uspgriedgedg  15971  usgrislfuspgrdom  15982  usgredg2en  15987  usgredgprv  15988  usgrpredgv  15990  usgredg  15992  usgrnloopv  15993  usgredgne  15996  usgredg3  16006  usgredgedg  16019  usgredgdomord  16022  bj-inex  16228  bj-nn0suc  16285  bj-nn0sucALT  16299  trilpolemeq1  16367  trilpolemlt1  16368  trirec0  16371  nconstwlpolemgt0  16391