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  6569  smores2  6570  smoel  6576  smoiso  6578  tfrlem1  6584  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemiubacc  6606  tfr1onlemsucaccv  6617  tfr1onlembfn  6620  tfr1onlemubacc  6622  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllemsucaccv  6630  tfrcllembfn  6633  tfrcllemubacc  6635  tfrcllemaccex  6637  tfrcllemres  6638  tfrcl  6640  frecrdg  6684  omv2  6743  nnasuc  6754  nnmsuc  6755  nnacom  6762  nnaass  6763  nnmass  6765  nntri1  6774  nndifsnid  6785  nnmordi  6794  swoer  6840  erth  6858  riinerm  6887  qliftlem  6892  ecovass  6923  ecoviass  6924  elmapssres  6959  fvixp  6991  f1domg  7050  domssr  7070  endomtr  7083  xpsnen2g  7133  enen1  7146  enen2  7147  domen1  7148  domen2  7149  mapen  7152  mapxpen  7154  ssenen  7158  phplem1  7159  fidifsnid  7179  findcard  7198  findcard2  7199  findcard2s  7200  fidcen  7209  relresfin  7270  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  9710  nnaddm1cl  9715  zdceq  9729  gtndiv  9751  prime  9755  msqznn  9756  btwnz  9775  uzss  9958  eluzadd  9966  nn0pzuz  10002  supinfneg  10010  infsupneg  10011  divfnzn  10036  qnegcl  10051  qreccl  10057  elpqb  10066  xaddass  10287  xleadd1a  10291  xlesubadd  10301  elico2  10355  iccss  10359  iccsupr  10384  elfz5  10436  fznn  10512  difelfznle  10558  fzoaddel  10621  elincfzoext  10627  qdceq  10695  qbtwnxr  10708  flqbi2  10746  adddivflid  10747  fldivnn0  10750  divfl0  10751  flqmulnn0  10754  fldivnn0le  10758  fldiv4p1lem1div2  10760  ceiqle  10770  flqdiv  10778  modqmulnn  10799  frecuzrdgtcl  10869  frecuzrdgsuc  10871  frecuzrdgdomlem  10874  frecuzrdgfunlem  10876  frecuzrdgsuctlem  10880  seqm1g  10931  seq3caopr2  10950  seqcaopr2g  10951  iseqf1olemkle  10954  seq3f1olemp  10972  seqf1oglem2  10977  seqf1og  10978  seq3id  10982  seq3z  10985  expap0  11026  mulexp  11035  mulexpzap  11036  expmul  11041  leexp1a  11051  expubnd  11053  zesq  11116  bernneq  11118  bernneq3  11120  modqexp  11124  facdiv  11197  facndiv  11198  faclbnd3  11202  faclbnd6  11203  bccmpl  11213  bcpasc  11225  bccl  11226  hashfibclem  11303  hashfibc  11304  seq3coll  11315  fundm2domnop  11322  wrdsymb1  11362  ccatfv0  11392  ccatrn  11398  ccat2s1cl  11422  lswccats1fst  11433  swrdspsleq  11460  pfxtrcfv  11486  pfxsuffeqwrdeq  11491  pfxlswccat  11506  wrdeqs1cat  11513  cats1un  11514  swrdccatin1  11518  pfxccatin12lem4  11519  swrdccatin2  11522  pfxccatin12  11526  swrdccat  11528  shftlem  11602  ovshftex  11605  shftval4  11614  shftf  11616  shftcan2  11621  crim  11644  mulreap  11650  remul2  11659  immul2  11666  cjexp  11679  caucvgre  11768  r19.2uz  11780  sqrtsq2  11830  absnid  11860  absexp  11867  nn0abscl  11873  abslt  11876  lenegsq  11883  cau3lem  11902  minmax  12019  xrmaxadd  12051  clim  12071  climshftlemg  12092  climcn1  12098  climcn1lem  12109  clim2ser  12127  clim2ser2  12128  iserex  12129  isermulc2  12130  climub  12134  climcaucn  12141  serf0  12142  summodclem3  12171  summodclem2a  12172  summodclem2  12173  summodc  12174  fsum3  12178  fsumf1o  12181  fisumss  12183  isumss2  12184  fsumcl2lem  12189  fsumadd  12197  fsumsplit  12198  isummulc2  12217  fsum2d  12226  fsummulc2  12239  telfsumo  12257  fsumparts  12261  hash2iun1dif1  12271  bcxmas  12280  isumshft  12281  isumsplit  12282  expcnvap0  12293  geolim  12302  geolim2  12303  cvgratnnlemmn  12316  cvgratnnlemseq  12317  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  clim2divap  12331  prodmodclem3  12366  prodmodclem2a  12367  fprodseq  12374  fprodf1o  12379  fprodmul  12382  fprodsplitdc  12387  efcllemp  12449  reefcl  12459  efcj  12464  efaddlem  12465  efexp  12473  reeftlcl  12480  eftlub  12481  efsep  12482  effsumlt  12483  eflegeo  12492  retanclap  12513  demoivre  12564  demoivreALT  12565  eirraplem  12568  dvdsval3  12582  p1modz1  12585  iddvdsexp  12606  alzdvds  12645  addmodlteqALT  12650  nnehalf  12695  nno  12697  ndvdsadd  12722  bitsp1e  12743  bitsp1o  12744  bitsinv1  12753  divgcdnnr  12777  neggcd  12784  gcdabs  12789  bezoutlemmain  12799  bezoutlemaz  12804  bezoutlembz  12805  gcdmultiplez  12822  gcdzeq  12823  dvdssq  12832  nninfctlemfo  12841  algrf  12847  algcvg  12850  algcvga  12853  algfx  12854  eucalgf  12857  eucalgcvga  12860  neglcm  12877  lcmabs  12878  lcmdvds  12881  lcmgcdeq  12885  qredeq  12898  isprm3  12920  coprm  12947  prmrp  12948  isprm6  12950  prmdvdsexpb  12952  rpexp  12956  cncongrprm  12960  sqrt2irraplemnn  12983  phibndlem  13022  phiprmpw  13028  eulerthlemh  13037  eulerthlemth  13038  fermltl  13040  prmdivdiv  13043  modprm1div  13054  m1dvdsndvds  13055  coprimeprodsq  13064  pczpre  13104  pczcl  13105  pcexp  13116  pczdvds  13121  pczndvds  13123  pczndvds2  13125  pcdvdsb  13127  pcneg  13132  pcprmpw  13141  difsqpwdvds  13145  pcmptcl  13149  pcprod  13153  fldivp1  13155  infpnlem2  13167  1arithlem4  13173  prmlem0  13248  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfrcn0  13330  ennnfonelemrn  13367  topnidg  13664  imasaddfnlemg  13693  imasaddflemg  13695  qusin  13705  mgmlrid  13757  mndass  13795  mhmco  13855  gzsumwcl  13860  gzsumwmhm  13861  grpass  13872  grpinvex  13873  dfgrp2  13890  grplid  13894  grprid  13895  grprcan  13900  grpinvssd  13940  grpinvval2  13946  mhmid  13976  mhmmnd  13977  ghmgrp  13979  mulgnn  13987  mulgnnp1  13991  mulgnegnn  13993  mulgnnsubcl  13995  mulgz  14011  issubg2m  14050  issubg4m  14054  subgintm  14059  nmzbi  14070  eqger  14085  eqgid  14087  eqgen  14088  qusgrp  14093  qusadd  14095  qusinv  14097  qussub  14098  ghminv  14111  ghmsub  14112  ghmrn  14118  resghm2b  14123  ghmf1  14134  conjsubg  14138  conjsubgen  14139  qusghm  14143  cntzi  14161  cntzsgrpcl  14166  cntzsubm  14169  cntzsubg  14170  cmncom  14194  ablsubadd  14205  ablsubsub23  14218  ghmcmn  14220  gzsumreidx  14230  gsummptfidmsplit  14253  gsumsubmfi  14267  prdsidlem  14299  prdsinvlem  14302  pwselbasb  14312  pwsplusgval  14314  pwsmulrval  14315  pwsinvg  14321  mgpress  14336  srg1expzeq1  14405  ringinvnz1ne0  14460  ringinvnzdiv  14461  dvdsrd  14509  dvdsunit  14527  unitinvcl  14538  unitinvinv  14539  unitlinv  14541  unitrinv  14542  rhmunitinv  14593  subrngintm  14628  subrg1  14647  subrguss  14652  subrginv  14653  subrgunit  14655  subrgugrp  14656  subrgintm  14659  resrhm  14664  resrhm2b  14665  lmodass  14747  lmodlcan  14748  lmod0vlid  14763  lmod0vrid  14764  lmod0vid  14765  lmodvs0  14767  lcomf  14772  lmodvnegcl  14773  lmodvnegid  14774  lmodvsubadd  14783  lmodsubid  14792  lss1d  14828  lspval  14835  ellspsn6  14853  lspsnneg  14865  sralmod  14895  dflidl2rng  14926  lidlacl  14929  dflidl2  14933  df2idl2  14954  qusmul2  14974  quscrng  14978  cnfldmulg  15021  znf1o  15094  znidom  15100  aspval  15123  asclghm  15133  issubassa2  15143  gsumbagdiagfi  15185  psrass1filem  15186  psraddcl  15193  psrmulvalfi  15197  psr0lid  15201  psrlidmfi  15208  mvrclfi  15226  mplsubgfilemcl  15232  tgss3  15321  clsval  15354  clsss3  15373  neiss2  15385  resttop  15413  resttopon2  15421  lmconst  15459  cnima  15463  cnntri  15467  cncnp  15473  cnrest  15478  cndis  15484  lmss  15489  lmff  15492  lmtopcnp  15493  txcnp  15514  upxp  15515  uptx  15517  cnmpt11  15526  hmeoima  15553  hmeoopn  15554  hmeocld  15555  hmeontr  15556  hmeoimaf1o  15557  mettri2  15605  met0  15607  metres2  15624  blpnf  15643  xblss2ps  15647  xblss2  15648  blbas  15676  blres  15677  xmetec  15680  mopnss  15693  xmstri2  15713  mstri2  15714  xmstri  15715  mstri  15716  xmstri3  15717  mstri3  15718  msrtri  15719  mopni3  15727  unimopn  15729  comet  15742  bdxmet  15744  climcncf  15827  dedekindeulemuub  15860  dedekindicclemuub  15869  ivthdichlem  15894  dvfgg  15931  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvfre  15953  dvmptfsum  15968  plyadd  15994  plymul  15995  reeff1olem  16014  reeff1o  16016  sinperlem  16052  abssinper  16090  reexplog  16118  relogexp  16119  cxpexpnn  16146  cxprec  16160  rpcxpmul2  16163  abscxp  16167  wilthlem1  16249  ppival2g  16267  sgmval2  16270  sgmnncl  16274  0sgmppw  16304  chtublem  16312  perfectlem1  16316  bposlem3  16330  bposlem5  16332  bposlem6  16333  lgsdir  16376  lgsprme0  16383  lgsdinn0  16389  gausslemma2dlem3  16404  gausslemma2dlem5a  16406  2lgslem1a2  16428  2lgslem1a  16429  2lgslem3  16442  2lgs  16445  umgredgprv  16578  umgrislfupgrdom  16594  uspgredgiedg  16641  uspgriedgedg  16642  usgrislfuspgrdom  16653  usgredg2en  16658  usgredgprv  16659  usgrpredgv  16661  usgredg  16663  usgrnloopv  16664  usgredgne  16667  usgredg3  16677  usgredgedg  16690  usgredgdomord  16693  usgr1vr  16711  subgruhgrfun  16731  subupgr  16736  subumgr  16737  subusgr  16738  umgrwlknloop  16831  wlkres  16842  clwwlkccatlem  16863  clwwlkccat  16864  depindlem1  16969  depindlem2  16970  depindlem3  16971  bj-inex  17155  bj-nn0suc  17212  bj-nn0sucALT  17226  trilpolemeq1  17313  trilpolemlt1  17314  trirec0  17317  nconstwlpolemgt0  17338