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  4215  otexg  4372  opelopabt  4406  sonr  4464  sotr  4465  issod  4466  so2nr  4468  so3nr  4469  ordelss  4526  onelon  4531  elrnmpt1s  5034  iota2  5370  funeu  5405  imadif  5464  fnbr  5488  feu  5577  f1ss  5607  f1ssres  5610  f1resf1  5611  dffo2  5622  foco  5629  foun  5661  fun11iun  5663  ffoss  5675  funbrfv  5742  fvco3  5779  fvopab6  5808  funfvbrb  5825  elpreima  5831  ffvelcdm  5844  ffvelcdmda  5846  dffo4  5859  fmptco  5877  fsn2  5885  fncofn  5896  fvconst2g  5932  fex  5950  funfvima  5953  f1elima  5982  f1ocnvfv1  5986  f1ocnvfv2  5987  cocan2  5997  foeqcnvco  5999  isocnv  6020  isores2  6022  isoini  6027  isoselem  6029  f1oiso  6035  f1ofveu  6076  eloprabga  6178  suppssof1  6324  ofco  6325  offveqb  6326  ofc1g  6328  ofc2g  6329  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  fnexALT  6344  f1dmex  6349  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  eqopi  6410  2ndrn  6421  fo2ndf  6467  suppval1  6483  ressuppss  6498  suppssrst  6505  suppssrgst  6506  smores3  6568  smores2  6569  smoel  6575  smoiso  6577  tfrlem1  6583  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemiubacc  6605  tfr1onlemsucaccv  6616  tfr1onlembfn  6619  tfr1onlemubacc  6621  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllemsucaccv  6629  tfrcllembfn  6632  tfrcllemubacc  6634  tfrcllemaccex  6636  tfrcllemres  6637  tfrcl  6639  frecrdg  6683  omv2  6742  nnasuc  6753  nnmsuc  6754  nnacom  6761  nnaass  6762  nnmass  6764  nntri1  6773  nndifsnid  6784  nnmordi  6793  swoer  6839  erth  6857  riinerm  6886  qliftlem  6891  ecovass  6922  ecoviass  6923  elmapssres  6958  fvixp  6989  f1domg  7048  domssr  7068  endomtr  7081  xpsnen2g  7131  enen1  7144  enen2  7145  domen1  7146  domen2  7147  mapen  7150  mapxpen  7152  ssenen  7156  phplem1  7157  fidifsnid  7177  findcard  7196  findcard2  7197  findcard2s  7198  fidcen  7207  relresfin  7268  fieq0  7315  isotilem  7352  supisolem  7354  inflbti  7370  ordiso2  7381  djuex  7389  updjudhcoinlf  7426  updjudhcoinrg  7427  updjud  7428  ctssdccl  7457  enumctlemm  7460  nnnninf  7472  finomni  7486  pm54.43  7542  acfun  7569  ccfunen  7636  cc2lem  7638  cc3  7640  addclpi  7700  addasspig  7703  mulasspig  7705  addnidpig  7709  nnppipi  7716  ltanqi  7775  ltmnqi  7776  ltexnqq  7781  archnqq  7790  prarloclemarch2  7792  enq0sym  7805  enq0tr  7807  nqnq0pi  7811  nqnq0  7814  mulcanenq0ec  7818  addclnq0  7824  nqpnq0nq  7826  distrnq0  7832  addassnq0lemcl  7834  addassnq0  7835  prubl  7859  prarloclemlt  7866  genpdf  7881  genipv  7882  genpelvl  7885  genpelvu  7886  genpml  7890  genpmu  7891  genprndl  7894  genprndu  7895  genpassl  7897  genpassu  7898  genpassg  7899  addnqprl  7902  addnqpru  7903  addlocpr  7909  nqprm  7915  nqprl  7924  nqpru  7925  mulnqprl  7941  mulnqpru  7942  mullocprlem  7943  mullocpr  7944  addcomprg  7951  mulcomprg  7953  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  ltprordil  7962  1idprl  7963  1idpru  7964  ltpopr  7968  ltsopr  7969  ltaddpr  7970  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  prplnqu  7993  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  aptiprleml  8012  aptiprlemu  8013  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemloc  8048  caucvgprlemladdrl  8051  caucvgprprlemml  8067  caucvgprprlemloc  8076  00sr  8142  map2psrprg  8178  suplocsrlempr  8180  suplocsrlem  8181  adddir  8323  axsuploc  8404  eqle  8423  le2tri3i  8441  mul4  8465  muladd11  8466  cnegexlem3  8510  addsub12  8546  2addsub  8547  addsubeq4  8548  subadd4  8577  negcon1  8585  negdi2  8591  negsubdi2  8592  neg2sub  8593  renegcl  8594  muladd  8718  subdir  8720  gt0ne0  8762  ltnegcon1  8798  lenegcon1  8801  eqord1  8818  eqord2  8819  recexre  8914  ltmul1  8928  recexap  8989  div12ap  9032  rerecapb  9181  p1le  9187  ltmul2  9194  gt0div  9208  ge0div  9209  zlem1lt  9712  nnaddm1cl  9717  zdceq  9731  gtndiv  9752  prime  9756  msqznn  9757  btwnz  9776  uzss  9959  eluzadd  9967  nn0pzuz  10003  supinfneg  10011  infsupneg  10012  divfnzn  10037  qnegcl  10052  qreccl  10058  elpqb  10067  xaddass  10288  xleadd1a  10292  xlesubadd  10302  elico2  10356  iccss  10360  iccsupr  10385  elfz5  10437  fznn  10513  difelfznle  10559  fzoaddel  10622  elincfzoext  10628  qdceq  10696  qbtwnxr  10709  flqbi2  10747  adddivflid  10748  fldivnn0  10751  divfl0  10752  flqmulnn0  10755  fldivnn0le  10759  fldiv4p1lem1div2  10761  ceiqle  10771  flqdiv  10779  modqmulnn  10800  frecuzrdgtcl  10870  frecuzrdgsuc  10872  frecuzrdgdomlem  10875  frecuzrdgfunlem  10877  frecuzrdgsuctlem  10881  seqm1g  10932  seq3caopr2  10951  seqcaopr2g  10952  iseqf1olemkle  10955  seq3f1olemp  10973  seqf1oglem2  10978  seqf1og  10979  seq3id  10983  seq3z  10986  expap0  11027  mulexp  11036  mulexpzap  11037  expmul  11042  leexp1a  11052  expubnd  11054  zesq  11117  bernneq  11119  bernneq3  11121  modqexp  11125  facdiv  11198  facndiv  11199  faclbnd3  11203  faclbnd6  11204  bccmpl  11214  bcpasc  11226  bccl  11227  hashfibclem  11304  hashfibc  11305  seq3coll  11316  fundm2domnop  11323  wrdsymb1  11363  ccatfv0  11393  ccatrn  11399  ccat2s1cl  11423  lswccats1fst  11434  swrdspsleq  11461  pfxtrcfv  11487  pfxsuffeqwrdeq  11492  pfxlswccat  11507  wrdeqs1cat  11514  cats1un  11515  swrdccatin1  11519  pfxccatin12lem4  11520  swrdccatin2  11523  pfxccatin12  11527  swrdccat  11529  shftlem  11603  ovshftex  11606  shftval4  11615  shftf  11617  shftcan2  11622  crim  11645  mulreap  11651  remul2  11660  immul2  11667  cjexp  11680  caucvgre  11769  r19.2uz  11781  sqrtsq2  11831  absnid  11861  absexp  11868  nn0abscl  11874  abslt  11877  lenegsq  11884  cau3lem  11903  minmax  12020  xrmaxadd  12052  clim  12072  climshftlemg  12093  climcn1  12099  climcn1lem  12110  clim2ser  12128  clim2ser2  12129  iserex  12130  isermulc2  12131  climub  12135  climcaucn  12142  serf0  12143  summodclem3  12172  summodclem2a  12173  summodclem2  12174  summodc  12175  fsum3  12179  fsumf1o  12182  fisumss  12184  isumss2  12185  fsumcl2lem  12190  fsumadd  12198  fsumsplit  12199  isummulc2  12218  fsum2d  12227  fsummulc2  12240  telfsumo  12258  fsumparts  12262  hash2iun1dif1  12272  bcxmas  12281  isumshft  12282  isumsplit  12283  expcnvap0  12294  geolim  12303  geolim2  12304  cvgratnnlemmn  12317  cvgratnnlemseq  12318  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  clim2divap  12332  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  fprodf1o  12380  fprodmul  12383  fprodsplitdc  12388  efcllemp  12450  reefcl  12460  efcj  12465  efaddlem  12466  efexp  12474  reeftlcl  12481  eftlub  12482  efsep  12483  effsumlt  12484  eflegeo  12493  retanclap  12514  demoivre  12565  demoivreALT  12566  eirraplem  12569  dvdsval3  12583  p1modz1  12586  iddvdsexp  12607  alzdvds  12646  addmodlteqALT  12651  nnehalf  12696  nno  12698  ndvdsadd  12723  bitsp1e  12744  bitsp1o  12745  bitsinv1  12754  divgcdnnr  12778  neggcd  12785  gcdabs  12790  bezoutlemmain  12800  bezoutlemaz  12805  bezoutlembz  12806  gcdmultiplez  12823  gcdzeq  12824  dvdssq  12833  nninfctlemfo  12842  algrf  12848  algcvg  12851  algcvga  12854  algfx  12855  eucalgf  12858  eucalgcvga  12861  neglcm  12878  lcmabs  12879  lcmdvds  12882  lcmgcdeq  12886  qredeq  12899  isprm3  12921  coprm  12948  prmrp  12949  isprm6  12951  prmdvdsexpb  12953  rpexp  12957  cncongrprm  12961  sqrt2irraplemnn  12984  phibndlem  13023  phiprmpw  13029  eulerthlemh  13038  eulerthlemth  13039  fermltl  13041  prmdivdiv  13044  modprm1div  13055  m1dvdsndvds  13056  coprimeprodsq  13065  pczpre  13105  pczcl  13106  pcexp  13117  pczdvds  13122  pczndvds  13124  pczndvds2  13126  pcdvdsb  13128  pcneg  13133  pcprmpw  13142  difsqpwdvds  13146  pcmptcl  13150  pcprod  13154  fldivp1  13156  infpnlem2  13168  1arithlem4  13174  prmlem0  13249  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfrcn0  13331  ennnfonelemrn  13368  topnidg  13665  imasaddfnlemg  13694  imasaddflemg  13696  qusin  13706  mgmlrid  13758  mndass  13796  mhmco  13856  gzsumwcl  13861  gzsumwmhm  13862  grpass  13873  grpinvex  13874  dfgrp2  13891  grplid  13895  grprid  13896  grprcan  13901  grpinvssd  13941  grpinvval2  13947  mhmid  13977  mhmmnd  13978  ghmgrp  13980  mulgnn  13988  mulgnnp1  13992  mulgnegnn  13994  mulgnnsubcl  13996  mulgz  14012  issubg2m  14051  issubg4m  14055  subgintm  14060  nmzbi  14071  eqger  14086  eqgid  14088  eqgen  14089  qusgrp  14094  qusadd  14096  qusinv  14098  qussub  14099  ghminv  14112  ghmsub  14113  ghmrn  14119  resghm2b  14124  ghmf1  14135  conjsubg  14139  conjsubgen  14140  qusghm  14144  cntzi  14162  cntzsgrpcl  14167  cntzsubm  14170  cntzsubg  14171  cmncom  14195  ablsubadd  14206  ablsubsub23  14219  ghmcmn  14221  gzsumreidx  14231  gsummptfidmsplit  14254  gsumsubmfi  14268  prdsidlem  14300  prdsinvlem  14303  pwselbasb  14313  pwsplusgval  14315  pwsmulrval  14316  pwsinvg  14322  mgpress  14337  srg1expzeq1  14406  ringinvnz1ne0  14461  ringinvnzdiv  14462  dvdsrd  14510  dvdsunit  14528  unitinvcl  14539  unitinvinv  14540  unitlinv  14542  unitrinv  14543  rhmunitinv  14594  subrngintm  14629  subrg1  14648  subrguss  14653  subrginv  14654  subrgunit  14656  subrgugrp  14657  subrgintm  14660  resrhm  14665  resrhm2b  14666  lmodass  14748  lmodlcan  14749  lmod0vlid  14764  lmod0vrid  14765  lmod0vid  14766  lmodvs0  14768  lcomf  14773  lmodvnegcl  14774  lmodvnegid  14775  lmodvsubadd  14784  lmodsubid  14793  lss1d  14829  lspval  14836  ellspsn6  14854  lspsnneg  14866  sralmod  14896  dflidl2rng  14927  lidlacl  14930  dflidl2  14934  df2idl2  14955  qusmul2  14975  quscrng  14979  cnfldmulg  15022  znf1o  15095  znidom  15101  aspval  15124  asclghm  15134  issubassa2  15144  gsumbagdiagfi  15176  psrass1filem  15177  psraddcl  15184  psrmulvalfi  15188  psr0lid  15192  psrlidmfi  15199  tgss3  15304  clsval  15337  clsss3  15356  neiss2  15368  resttop  15396  resttopon2  15404  lmconst  15442  cnima  15446  cnntri  15450  cncnp  15456  cnrest  15461  cndis  15467  lmss  15472  lmff  15475  lmtopcnp  15476  txcnp  15497  upxp  15498  uptx  15500  cnmpt11  15509  hmeoima  15536  hmeoopn  15537  hmeocld  15538  hmeontr  15539  hmeoimaf1o  15540  mettri2  15588  met0  15590  metres2  15607  blpnf  15626  xblss2ps  15630  xblss2  15631  blbas  15659  blres  15660  xmetec  15663  mopnss  15676  xmstri2  15696  mstri2  15697  xmstri  15698  mstri  15699  xmstri3  15700  mstri3  15701  msrtri  15702  mopni3  15710  unimopn  15712  comet  15725  bdxmet  15727  climcncf  15810  dedekindeulemuub  15843  dedekindicclemuub  15852  ivthdichlem  15877  dvfgg  15914  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvfre  15936  dvmptfsum  15951  plyadd  15977  plymul  15978  reeff1olem  15997  reeff1o  15999  sinperlem  16035  abssinper  16073  reexplog  16101  relogexp  16102  cxpexpnn  16129  cxprec  16143  rpcxpmul2  16146  abscxp  16150  wilthlem1  16232  ppival2g  16250  sgmval2  16253  sgmnncl  16257  0sgmppw  16287  chtublem  16295  perfectlem1  16299  bposlem3  16313  bposlem5  16315  bposlem6  16316  lgsdir  16359  lgsprme0  16366  lgsdinn0  16372  gausslemma2dlem3  16387  gausslemma2dlem5a  16389  2lgslem1a2  16411  2lgslem1a  16412  2lgslem3  16425  2lgs  16428  umgredgprv  16561  umgrislfupgrdom  16577  uspgredgiedg  16624  uspgriedgedg  16625  usgrislfuspgrdom  16636  usgredg2en  16641  usgredgprv  16642  usgrpredgv  16644  usgredg  16646  usgrnloopv  16647  usgredgne  16650  usgredg3  16660  usgredgedg  16673  usgredgdomord  16676  usgr1vr  16694  subgruhgrfun  16714  subupgr  16719  subumgr  16720  subusgr  16721  umgrwlknloop  16814  wlkres  16825  clwwlkccatlem  16846  clwwlkccat  16847  depindlem1  16952  depindlem2  16953  depindlem3  16954  bj-inex  17138  bj-nn0suc  17195  bj-nn0sucALT  17209  trilpolemeq1  17296  trilpolemlt1  17297  trirec0  17300  nconstwlpolemgt0  17321