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  3165  csbnestgf  3178  reuss2  3485  mpteq12  4170  otexg  4320  opelopabt  4354  sonr  4412  sotr  4413  issod  4414  so2nr  4416  so3nr  4417  ordelss  4474  onelon  4479  elrnmpt1s  4980  iota2  5314  funeu  5349  imadif  5407  fnbr  5431  feu  5516  f1ss  5545  f1ssres  5548  f1resf1  5549  dffo2  5560  foco  5567  foun  5599  fun11iun  5601  ffoss  5612  funbrfv  5678  fvco3  5713  fvopab6  5739  funfvbrb  5756  elpreima  5762  ffvelcdm  5776  ffvelcdmda  5778  dffo4  5791  fmptco  5809  fsn2  5817  fncofn  5827  fvconst2g  5863  fex  5878  funfvima  5881  f1elima  5909  f1ocnvfv1  5913  f1ocnvfv2  5914  cocan2  5924  foeqcnvco  5926  isocnv  5947  isores2  5949  isoini  5954  isoselem  5956  f1oiso  5962  f1ofveu  6001  eloprabga  6103  suppssof1  6248  ofco  6249  offveqb  6250  ofc1g  6252  ofc2g  6253  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  fnexALT  6268  f1dmex  6273  ot1stg  6310  ot2ndg  6311  ot3rdgg  6312  eqopi  6330  2ndrn  6341  fo2ndf  6387  smores3  6454  smores2  6455  smoel  6461  smoiso  6463  tfrlem1  6469  tfrlemisucaccv  6486  tfrlemibxssdm  6488  tfrlemiubacc  6491  tfr1onlemsucaccv  6502  tfr1onlembfn  6505  tfr1onlemubacc  6507  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllemsucaccv  6515  tfrcllembfn  6518  tfrcllemubacc  6520  tfrcllemaccex  6522  tfrcllemres  6523  tfrcl  6525  frecrdg  6569  omv2  6628  nnasuc  6639  nnmsuc  6640  nnacom  6647  nnaass  6648  nnmass  6650  nntri1  6659  nndifsnid  6670  nnmordi  6679  swoer  6725  erth  6743  riinerm  6772  qliftlem  6777  ecovass  6808  ecoviass  6809  elmapssres  6837  fvixp  6867  f1domg  6926  domssr  6946  endomtr  6959  xpsnen2g  7008  enen1  7021  enen2  7022  domen1  7023  domen2  7024  mapen  7027  mapxpen  7029  ssenen  7032  phplem1  7033  fidifsnid  7053  findcard  7070  findcard2  7071  findcard2s  7072  fidcen  7081  fieq0  7166  isotilem  7196  supisolem  7198  inflbti  7214  ordiso2  7225  djuex  7233  updjudhcoinlf  7270  updjudhcoinrg  7271  updjud  7272  ctssdccl  7301  enumctlemm  7304  nnnninf  7316  finomni  7330  pm54.43  7386  acfun  7412  ccfunen  7473  cc2lem  7475  cc3  7477  addclpi  7537  addasspig  7540  mulasspig  7542  addnidpig  7546  nnppipi  7553  ltanqi  7612  ltmnqi  7613  ltexnqq  7618  archnqq  7627  prarloclemarch2  7629  enq0sym  7642  enq0tr  7644  nqnq0pi  7648  nqnq0  7651  mulcanenq0ec  7655  addclnq0  7661  nqpnq0nq  7663  distrnq0  7669  addassnq0lemcl  7671  addassnq0  7672  prubl  7696  prarloclemlt  7703  genpdf  7718  genipv  7719  genpelvl  7722  genpelvu  7723  genpml  7727  genpmu  7728  genprndl  7731  genprndu  7732  genpassl  7734  genpassu  7735  genpassg  7736  addnqprl  7739  addnqpru  7740  addlocpr  7746  nqprm  7752  nqprl  7761  nqpru  7762  mulnqprl  7778  mulnqpru  7779  mullocprlem  7780  mullocpr  7781  addcomprg  7788  mulcomprg  7790  distrlem1prl  7792  distrlem1pru  7793  distrlem4prl  7794  distrlem4pru  7795  ltprordil  7799  1idprl  7800  1idpru  7801  ltpopr  7805  ltsopr  7806  ltaddpr  7807  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  prplnqu  7830  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1l  7845  recexprlemss1u  7846  aptiprleml  7849  aptiprlemu  7850  cauappcvgprlemloc  7862  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemloc  7885  caucvgprlemladdrl  7888  caucvgprprlemml  7904  caucvgprprlemloc  7913  00sr  7979  map2psrprg  8015  suplocsrlempr  8017  suplocsrlem  8018  adddir  8160  axsuploc  8242  eqle  8261  le2tri3i  8278  mul4  8301  muladd11  8302  cnegexlem3  8346  addsub12  8382  2addsub  8383  addsubeq4  8384  subadd4  8413  negcon1  8421  negdi2  8427  negsubdi2  8428  neg2sub  8429  renegcl  8430  muladd  8553  subdir  8555  gt0ne0  8597  ltnegcon1  8633  lenegcon1  8636  eqord1  8653  eqord2  8654  recexre  8748  ltmul1  8762  recexap  8823  div12ap  8864  rerecapb  9013  p1le  9019  ltmul2  9026  gt0div  9040  ge0div  9041  zlem1lt  9526  nnaddm1cl  9531  zdceq  9545  gtndiv  9565  prime  9569  msqznn  9570  btwnz  9589  uzss  9767  eluzadd  9775  nn0pzuz  9811  supinfneg  9819  infsupneg  9820  divfnzn  9845  qnegcl  9860  qreccl  9866  elpqb  9874  xaddass  10094  xleadd1a  10098  xlesubadd  10108  elico2  10162  iccss  10166  iccsupr  10191  elfz5  10242  fznn  10314  difelfznle  10360  fzoaddel  10422  elincfzoext  10428  qdceq  10494  qbtwnxr  10507  flqbi2  10541  adddivflid  10542  fldivnn0  10545  divfl0  10546  flqmulnn0  10549  fldivnn0le  10553  fldiv4p1lem1div2  10555  ceiqle  10565  flqdiv  10573  modqmulnn  10594  frecuzrdgtcl  10664  frecuzrdgsuc  10666  frecuzrdgdomlem  10669  frecuzrdgfunlem  10671  frecuzrdgsuctlem  10675  seqm1g  10726  seq3caopr2  10745  seqcaopr2g  10746  iseqf1olemkle  10749  seq3f1olemp  10767  seqf1oglem2  10772  seqf1og  10773  seq3id  10777  seq3z  10780  expap0  10821  mulexp  10830  mulexpzap  10831  expmul  10836  leexp1a  10846  expubnd  10848  zesq  10910  bernneq  10912  bernneq3  10914  modqexp  10918  facdiv  10990  facndiv  10991  faclbnd3  10995  faclbnd6  10996  bccmpl  11006  bcpasc  11018  bccl  11019  seq3coll  11096  fundm2domnop  11100  wrdsymb1  11140  ccatfv0  11170  ccatrn  11176  ccat2s1cl  11200  lswccats1fst  11211  swrdspsleq  11238  pfxtrcfv  11264  pfxsuffeqwrdeq  11269  pfxlswccat  11284  wrdeqs1cat  11291  cats1un  11292  swrdccatin1  11296  pfxccatin12lem4  11297  swrdccatin2  11300  pfxccatin12  11304  swrdccat  11306  shftlem  11367  ovshftex  11370  shftval4  11379  shftf  11381  shftcan2  11386  crim  11409  mulreap  11415  remul2  11424  immul2  11431  cjexp  11444  caucvgre  11532  r19.2uz  11544  sqrtsq2  11594  absnid  11624  absexp  11630  nn0abscl  11636  abslt  11639  lenegsq  11646  cau3lem  11665  minmax  11781  xrmaxadd  11812  clim  11832  climshftlemg  11853  climcn1  11859  climcn1lem  11870  clim2ser  11888  clim2ser2  11889  iserex  11890  isermulc2  11891  climub  11895  climcaucn  11902  serf0  11903  summodclem3  11931  summodclem2a  11932  summodclem2  11933  summodc  11934  fsum3  11938  fsumf1o  11941  fisumss  11943  isumss2  11944  fsumcl2lem  11949  fsumadd  11957  fsumsplit  11958  isummulc2  11977  fsum2d  11986  fsummulc2  11999  telfsumo  12017  fsumparts  12021  hash2iun1dif1  12031  bcxmas  12040  isumshft  12041  isumsplit  12042  expcnvap0  12053  geolim  12062  geolim2  12063  cvgratnnlemmn  12076  cvgratnnlemseq  12077  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  clim2divap  12091  prodmodclem3  12126  prodmodclem2a  12127  fprodseq  12134  fprodf1o  12139  fprodmul  12142  fprodsplitdc  12147  efcllemp  12209  reefcl  12219  efcj  12224  efaddlem  12225  efexp  12233  reeftlcl  12240  eftlub  12241  efsep  12242  effsumlt  12243  eflegeo  12252  retanclap  12273  demoivre  12324  demoivreALT  12325  eirraplem  12328  dvdsval3  12342  p1modz1  12345  iddvdsexp  12366  alzdvds  12405  addmodlteqALT  12410  nnehalf  12455  nno  12457  ndvdsadd  12482  bitsp1e  12503  bitsp1o  12504  bitsinv1  12513  divgcdnnr  12537  neggcd  12544  gcdabs  12549  bezoutlemmain  12559  bezoutlemaz  12564  bezoutlembz  12565  gcdmultiplez  12582  gcdzeq  12583  dvdssq  12592  nninfctlemfo  12601  algrf  12607  algcvg  12610  algcvga  12613  algfx  12614  eucalgf  12617  eucalgcvga  12620  neglcm  12637  lcmabs  12638  lcmdvds  12641  lcmgcdeq  12645  qredeq  12658  isprm3  12680  coprm  12706  prmrp  12707  isprm6  12709  prmdvdsexpb  12711  rpexp  12715  cncongrprm  12719  sqrt2irraplemnn  12741  phibndlem  12778  phiprmpw  12784  eulerthlemh  12793  eulerthlemth  12794  fermltl  12796  prmdivdiv  12799  modprm1div  12810  m1dvdsndvds  12811  coprimeprodsq  12820  pczpre  12860  pczcl  12861  pcexp  12872  pczdvds  12877  pczndvds  12879  pczndvds2  12881  pcdvdsb  12883  pcneg  12888  pcprmpw  12897  difsqpwdvds  12901  pcmptcl  12905  pcprod  12909  fldivp1  12911  infpnlem2  12923  1arithlem4  12929  ennnfonelemrn  13030  topnidg  13325  pwselbasb  13366  pwsplusgval  13368  pwsmulrval  13369  imasaddfnlemg  13387  imasaddflemg  13389  qusin  13399  mgmlrid  13452  mndass  13497  prdsidlem  13520  mhmco  13563  gsumsubm  13567  gsumwcl  13570  gsumwmhm  13571  grpass  13582  grpinvex  13583  dfgrp2  13600  grplid  13604  grprid  13605  grprcan  13610  grpinvssd  13650  grpinvval2  13656  prdsinvlem  13681  pwsinvg  13685  mhmid  13692  mhmmnd  13693  ghmgrp  13695  mulgnn  13703  mulgnnp1  13707  mulgnegnn  13709  mulgnnsubcl  13711  mulgz  13727  issubg2m  13766  issubg4m  13770  subgintm  13775  nmzbi  13786  eqger  13801  eqgid  13803  eqgen  13804  qusgrp  13809  qusadd  13811  qusinv  13813  qussub  13814  ghminv  13827  ghmsub  13828  ghmrn  13834  resghm2b  13839  ghmf1  13850  conjsubg  13854  conjsubgen  13855  qusghm  13859  cmncom  13879  ablsubadd  13889  ablsubsub23  13902  ghmcmn  13904  gsumfzreidx  13914  mgpress  13934  srg1expzeq1  13998  ringinvnz1ne0  14052  ringinvnzdiv  14053  dvdsrd  14098  dvdsunit  14116  unitinvcl  14127  unitinvinv  14128  unitlinv  14130  unitrinv  14131  rhmunitinv  14182  subrngintm  14216  subrg1  14235  subrguss  14240  subrginv  14241  subrgunit  14243  subrgugrp  14244  subrgintm  14247  resrhm  14252  resrhm2b  14253  lmodass  14307  lmodlcan  14308  lmod0vlid  14322  lmod0vrid  14323  lmod0vid  14324  lmodvs0  14326  lcomf  14331  lmodvnegcl  14332  lmodvnegid  14333  lmodvsubadd  14342  lmodsubid  14351  lss1d  14387  lspval  14394  lspsnel6  14412  lspsnneg  14424  sralmod  14454  dflidl2rng  14485  lidlacl  14488  dflidl2  14492  df2idl2  14513  qusmul2  14533  quscrng  14537  cnfldmulg  14580  znf1o  14655  znidom  14661  psraddcl  14684  psr0lid  14686  tgss3  14792  clsval  14825  clsss3  14844  neiss2  14856  resttop  14884  resttopon2  14892  lmconst  14930  cnima  14934  cnntri  14938  cncnp  14944  cnrest  14949  cndis  14955  lmss  14960  lmff  14963  lmtopcnp  14964  txcnp  14985  upxp  14986  uptx  14988  cnmpt11  14997  hmeoima  15024  hmeoopn  15025  hmeocld  15026  hmeontr  15027  hmeoimaf1o  15028  mettri2  15076  met0  15078  metres2  15095  blpnf  15114  xblss2ps  15118  xblss2  15119  blbas  15147  blres  15148  xmetec  15151  mopnss  15164  xmstri2  15184  mstri2  15185  xmstri  15186  mstri  15187  xmstri3  15188  mstri3  15189  msrtri  15190  mopni3  15198  unimopn  15200  comet  15213  bdxmet  15215  climcncf  15298  dedekindeulemuub  15331  dedekindicclemuub  15340  ivthdichlem  15365  dvfgg  15402  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvfre  15424  dvmptfsum  15439  plyadd  15465  plymul  15466  reeff1olem  15485  reeff1o  15487  sinperlem  15522  abssinper  15560  reexplog  15585  relogexp  15586  cxpexpnn  15610  cxprec  15624  rpcxpmul2  15627  abscxp  15629  wilthlem1  15694  sgmval2  15698  sgmnncl  15702  0sgmppw  15707  perfectlem1  15713  lgsdir  15754  lgsprme0  15761  lgsdinn0  15767  gausslemma2dlem3  15782  gausslemma2dlem5a  15784  2lgslem1a2  15806  2lgslem1a  15807  2lgslem3  15820  2lgs  15823  umgredgprv  15956  umgrislfupgrdom  15970  uspgredgiedg  16017  uspgriedgedg  16018  usgrislfuspgrdom  16029  usgredg2en  16034  usgredgprv  16035  usgrpredgv  16037  usgredg  16039  usgrnloopv  16040  usgredgne  16043  usgredg3  16053  usgredgedg  16066  usgredgdomord  16069  usgr1vr  16087  umgrwlknloop  16165  wlkres  16174  clwwlkccatlem  16195  clwwlkccat  16196  bj-inex  16438  bj-nn0suc  16495  bj-nn0sucALT  16509  trilpolemeq1  16580  trilpolemlt1  16581  trirec0  16584  nconstwlpolemgt0  16604