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  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  4212  otexg  4368  opelopabt  4402  sonr  4460  sotr  4461  issod  4462  so2nr  4464  so3nr  4465  ordelss  4522  onelon  4527  elrnmpt1s  5030  iota2  5365  funeu  5400  imadif  5459  fnbr  5483  feu  5572  f1ss  5602  f1ssres  5605  f1resf1  5606  dffo2  5617  foco  5624  foun  5656  fun11iun  5658  ffoss  5670  funbrfv  5736  fvco3  5773  fvopab6  5799  funfvbrb  5816  elpreima  5822  ffvelcdm  5835  ffvelcdmda  5837  dffo4  5850  fmptco  5868  fsn2  5876  fncofn  5887  fvconst2g  5923  fex  5940  funfvima  5943  f1elima  5972  f1ocnvfv1  5976  f1ocnvfv2  5977  cocan2  5987  foeqcnvco  5989  isocnv  6010  isores2  6012  isoini  6017  isoselem  6019  f1oiso  6025  f1ofveu  6066  eloprabga  6168  suppssof1  6313  ofco  6314  offveqb  6315  ofc1g  6317  ofc2g  6318  caofid0l  6322  caofid0r  6323  caofid1  6324  caofid2  6325  fnexALT  6333  f1dmex  6338  ot1stg  6379  ot2ndg  6380  ot3rdgg  6381  eqopi  6399  2ndrn  6410  fo2ndf  6456  suppval1  6472  ressuppss  6487  suppssrst  6494  suppssrgst  6495  smores3  6557  smores2  6558  smoel  6564  smoiso  6566  tfrlem1  6572  tfrlemisucaccv  6589  tfrlemibxssdm  6591  tfrlemiubacc  6594  tfr1onlemsucaccv  6605  tfr1onlembfn  6608  tfr1onlemubacc  6610  tfr1onlemaccex  6612  tfr1onlemres  6613  tfrcllemsucaccv  6618  tfrcllembfn  6621  tfrcllemubacc  6623  tfrcllemaccex  6625  tfrcllemres  6626  tfrcl  6628  frecrdg  6672  omv2  6731  nnasuc  6742  nnmsuc  6743  nnacom  6750  nnaass  6751  nnmass  6753  nntri1  6762  nndifsnid  6773  nnmordi  6782  swoer  6828  erth  6846  riinerm  6875  qliftlem  6880  ecovass  6911  ecoviass  6912  elmapssres  6947  fvixp  6978  f1domg  7037  domssr  7057  endomtr  7070  xpsnen2g  7120  enen1  7133  enen2  7134  domen1  7135  domen2  7136  mapen  7139  mapxpen  7141  ssenen  7145  phplem1  7146  fidifsnid  7166  findcard  7185  findcard2  7186  findcard2s  7187  fidcen  7196  fieq0  7303  isotilem  7339  supisolem  7341  inflbti  7357  ordiso2  7368  djuex  7376  updjudhcoinlf  7413  updjudhcoinrg  7414  updjud  7415  ctssdccl  7444  enumctlemm  7447  nnnninf  7459  finomni  7473  pm54.43  7529  acfun  7556  ccfunen  7623  cc2lem  7625  cc3  7627  addclpi  7687  addasspig  7690  mulasspig  7692  addnidpig  7696  nnppipi  7703  ltanqi  7762  ltmnqi  7763  ltexnqq  7768  archnqq  7777  prarloclemarch2  7779  enq0sym  7792  enq0tr  7794  nqnq0pi  7798  nqnq0  7801  mulcanenq0ec  7805  addclnq0  7811  nqpnq0nq  7813  distrnq0  7819  addassnq0lemcl  7821  addassnq0  7822  prubl  7846  prarloclemlt  7853  genpdf  7868  genipv  7869  genpelvl  7872  genpelvu  7873  genpml  7877  genpmu  7878  genprndl  7881  genprndu  7882  genpassl  7884  genpassu  7885  genpassg  7886  addnqprl  7889  addnqpru  7890  addlocpr  7896  nqprm  7902  nqprl  7911  nqpru  7912  mulnqprl  7928  mulnqpru  7929  mullocprlem  7930  mullocpr  7931  addcomprg  7938  mulcomprg  7940  distrlem1prl  7942  distrlem1pru  7943  distrlem4prl  7944  distrlem4pru  7945  ltprordil  7949  1idprl  7950  1idpru  7951  ltpopr  7955  ltsopr  7956  ltaddpr  7957  ltexprlemm  7960  ltexprlemopl  7961  ltexprlemlol  7962  ltexprlemopu  7963  ltexprlemupu  7964  ltexprlemdisj  7966  ltexprlemloc  7967  ltexprlemfl  7969  ltexprlemrl  7970  ltexprlemfu  7971  ltexprlemru  7972  addcanprleml  7974  addcanprlemu  7975  prplnqu  7980  recexprlemloc  7991  recexprlem1ssl  7993  recexprlem1ssu  7994  recexprlemss1l  7995  recexprlemss1u  7996  aptiprleml  7999  aptiprlemu  8000  cauappcvgprlemloc  8012  cauappcvgprlemladdru  8016  cauappcvgprlemladdrl  8017  caucvgprlemloc  8035  caucvgprlemladdrl  8038  caucvgprprlemml  8054  caucvgprprlemloc  8063  00sr  8129  map2psrprg  8165  suplocsrlempr  8167  suplocsrlem  8168  adddir  8310  axsuploc  8391  eqle  8410  le2tri3i  8427  mul4  8451  muladd11  8452  cnegexlem3  8496  addsub12  8532  2addsub  8533  addsubeq4  8534  subadd4  8563  negcon1  8571  negdi2  8577  negsubdi2  8578  neg2sub  8579  renegcl  8580  muladd  8704  subdir  8706  gt0ne0  8748  ltnegcon1  8784  lenegcon1  8787  eqord1  8804  eqord2  8805  recexre  8899  ltmul1  8913  recexap  8974  div12ap  9017  rerecapb  9166  p1le  9172  ltmul2  9179  gt0div  9193  ge0div  9194  zlem1lt  9683  nnaddm1cl  9688  zdceq  9702  gtndiv  9723  prime  9727  msqznn  9728  btwnz  9747  uzss  9925  eluzadd  9933  nn0pzuz  9969  supinfneg  9977  infsupneg  9978  divfnzn  10003  qnegcl  10018  qreccl  10024  elpqb  10032  xaddass  10253  xleadd1a  10257  xlesubadd  10267  elico2  10321  iccss  10325  iccsupr  10350  elfz5  10402  fznn  10477  difelfznle  10523  fzoaddel  10586  elincfzoext  10592  qdceq  10660  qbtwnxr  10673  flqbi2  10707  adddivflid  10708  fldivnn0  10711  divfl0  10712  flqmulnn0  10715  fldivnn0le  10719  fldiv4p1lem1div2  10721  ceiqle  10731  flqdiv  10739  modqmulnn  10760  frecuzrdgtcl  10830  frecuzrdgsuc  10832  frecuzrdgdomlem  10835  frecuzrdgfunlem  10837  frecuzrdgsuctlem  10841  seqm1g  10892  seq3caopr2  10911  seqcaopr2g  10912  iseqf1olemkle  10915  seq3f1olemp  10933  seqf1oglem2  10938  seqf1og  10939  seq3id  10943  seq3z  10946  expap0  10987  mulexp  10996  mulexpzap  10997  expmul  11002  leexp1a  11012  expubnd  11014  zesq  11077  bernneq  11079  bernneq3  11081  modqexp  11085  facdiv  11157  facndiv  11158  faclbnd3  11162  faclbnd6  11163  bccmpl  11173  bcpasc  11185  bccl  11186  hashfibclem  11263  hashfibc  11264  seq3coll  11275  fundm2domnop  11282  wrdsymb1  11322  ccatfv0  11352  ccatrn  11358  ccat2s1cl  11382  lswccats1fst  11393  swrdspsleq  11420  pfxtrcfv  11446  pfxsuffeqwrdeq  11451  pfxlswccat  11466  wrdeqs1cat  11473  cats1un  11474  swrdccatin1  11478  pfxccatin12lem4  11479  swrdccatin2  11482  pfxccatin12  11486  swrdccat  11488  shftlem  11562  ovshftex  11565  shftval4  11574  shftf  11576  shftcan2  11581  crim  11604  mulreap  11610  remul2  11619  immul2  11626  cjexp  11639  caucvgre  11728  r19.2uz  11740  sqrtsq2  11790  absnid  11820  absexp  11826  nn0abscl  11832  abslt  11835  lenegsq  11842  cau3lem  11861  minmax  11977  xrmaxadd  12008  clim  12028  climshftlemg  12049  climcn1  12055  climcn1lem  12066  clim2ser  12084  clim2ser2  12085  iserex  12086  isermulc2  12087  climub  12091  climcaucn  12098  serf0  12099  summodclem3  12128  summodclem2a  12129  summodclem2  12130  summodc  12131  fsum3  12135  fsumf1o  12138  fisumss  12140  isumss2  12141  fsumcl2lem  12146  fsumadd  12154  fsumsplit  12155  isummulc2  12174  fsum2d  12183  fsummulc2  12196  telfsumo  12214  fsumparts  12218  hash2iun1dif1  12228  bcxmas  12237  isumshft  12238  isumsplit  12239  expcnvap0  12250  geolim  12259  geolim2  12260  cvgratnnlemmn  12273  cvgratnnlemseq  12274  mertenslemi1  12283  mertenslem2  12284  mertensabs  12285  clim2divap  12288  prodmodclem3  12323  prodmodclem2a  12324  fprodseq  12331  fprodf1o  12336  fprodmul  12339  fprodsplitdc  12344  efcllemp  12406  reefcl  12416  efcj  12421  efaddlem  12422  efexp  12430  reeftlcl  12437  eftlub  12438  efsep  12439  effsumlt  12440  eflegeo  12449  retanclap  12470  demoivre  12521  demoivreALT  12522  eirraplem  12525  dvdsval3  12539  p1modz1  12542  iddvdsexp  12563  alzdvds  12602  addmodlteqALT  12607  nnehalf  12652  nno  12654  ndvdsadd  12679  bitsp1e  12700  bitsp1o  12701  bitsinv1  12710  divgcdnnr  12734  neggcd  12741  gcdabs  12746  bezoutlemmain  12756  bezoutlemaz  12761  bezoutlembz  12762  gcdmultiplez  12779  gcdzeq  12780  dvdssq  12789  nninfctlemfo  12798  algrf  12804  algcvg  12807  algcvga  12810  algfx  12811  eucalgf  12814  eucalgcvga  12817  neglcm  12834  lcmabs  12835  lcmdvds  12838  lcmgcdeq  12842  qredeq  12855  isprm3  12877  coprm  12903  prmrp  12904  isprm6  12906  prmdvdsexpb  12908  rpexp  12912  cncongrprm  12916  sqrt2irraplemnn  12938  phibndlem  12975  phiprmpw  12981  eulerthlemh  12990  eulerthlemth  12991  fermltl  12993  prmdivdiv  12996  modprm1div  13007  m1dvdsndvds  13008  coprimeprodsq  13017  pczpre  13057  pczcl  13058  pcexp  13069  pczdvds  13074  pczndvds  13076  pczndvds2  13078  pcdvdsb  13080  pcneg  13085  pcprmpw  13094  difsqpwdvds  13098  pcmptcl  13102  pcprod  13106  fldivp1  13108  infpnlem2  13120  1arithlem4  13126  ballotfilem2  13209  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemfrcn0  13254  ennnfonelemrn  13291  topnidg  13586  imasaddfnlemg  13615  imasaddflemg  13617  qusin  13627  mgmlrid  13679  mndass  13717  mhmco  13777  gzsumwcl  13782  gzsumwmhm  13783  grpass  13794  grpinvex  13795  dfgrp2  13812  grplid  13816  grprid  13817  grprcan  13822  grpinvssd  13862  grpinvval2  13868  mhmid  13898  mhmmnd  13899  ghmgrp  13901  mulgnn  13909  mulgnnp1  13913  mulgnegnn  13915  mulgnnsubcl  13917  mulgz  13933  issubg2m  13972  issubg4m  13976  subgintm  13981  nmzbi  13992  eqger  14007  eqgid  14009  eqgen  14010  qusgrp  14015  qusadd  14017  qusinv  14019  qussub  14020  ghminv  14033  ghmsub  14034  ghmrn  14040  resghm2b  14045  ghmf1  14056  conjsubg  14060  conjsubgen  14061  qusghm  14065  cmncom  14085  ablsubadd  14096  ablsubsub23  14109  ghmcmn  14111  gzsumreidx  14121  gsumsubmfi  14148  prdsidlem  14173  prdsinvlem  14176  pwselbasb  14186  pwsplusgval  14188  pwsmulrval  14189  pwsinvg  14195  mgpress  14208  srg1expzeq1  14276  ringinvnz1ne0  14330  ringinvnzdiv  14331  dvdsrd  14377  dvdsunit  14395  unitinvcl  14406  unitinvinv  14407  unitlinv  14409  unitrinv  14410  rhmunitinv  14461  subrngintm  14496  subrg1  14515  subrguss  14520  subrginv  14521  subrgunit  14523  subrgugrp  14524  subrgintm  14527  resrhm  14532  resrhm2b  14533  lmodass  14615  lmodlcan  14616  lmod0vlid  14630  lmod0vrid  14631  lmod0vid  14632  lmodvs0  14634  lcomf  14639  lmodvnegcl  14640  lmodvnegid  14641  lmodvsubadd  14650  lmodsubid  14659  lss1d  14695  lspval  14702  lspsnel6  14720  lspsnneg  14732  sralmod  14762  dflidl2rng  14793  lidlacl  14796  dflidl2  14800  df2idl2  14821  qusmul2  14841  quscrng  14845  cnfldmulg  14888  znf1o  14961  znidom  14967  psraddcl  14997  psr0lid  14999  tgss3  15105  clsval  15138  clsss3  15157  neiss2  15169  resttop  15197  resttopon2  15205  lmconst  15243  cnima  15247  cnntri  15251  cncnp  15257  cnrest  15262  cndis  15268  lmss  15273  lmff  15276  lmtopcnp  15277  txcnp  15298  upxp  15299  uptx  15301  cnmpt11  15310  hmeoima  15337  hmeoopn  15338  hmeocld  15339  hmeontr  15340  hmeoimaf1o  15341  mettri2  15389  met0  15391  metres2  15408  blpnf  15427  xblss2ps  15431  xblss2  15432  blbas  15460  blres  15461  xmetec  15464  mopnss  15477  xmstri2  15497  mstri2  15498  xmstri  15499  mstri  15500  xmstri3  15501  mstri3  15502  msrtri  15503  mopni3  15511  unimopn  15513  comet  15526  bdxmet  15528  climcncf  15611  dedekindeulemuub  15644  dedekindicclemuub  15653  ivthdichlem  15678  dvfgg  15715  dvidlemap  15718  dvidrelem  15719  dvidsslem  15720  dvfre  15737  dvmptfsum  15752  plyadd  15778  plymul  15779  reeff1olem  15798  reeff1o  15800  sinperlem  15835  abssinper  15873  reexplog  15898  relogexp  15899  cxpexpnn  15924  cxprec  15938  rpcxpmul2  15941  abscxp  15943  wilthlem1  16011  sgmval2  16015  sgmnncl  16019  0sgmppw  16024  perfectlem1  16030  lgsdir  16071  lgsprme0  16078  lgsdinn0  16084  gausslemma2dlem3  16099  gausslemma2dlem5a  16101  2lgslem1a2  16123  2lgslem1a  16124  2lgslem3  16137  2lgs  16140  umgredgprv  16273  umgrislfupgrdom  16289  uspgredgiedg  16336  uspgriedgedg  16337  usgrislfuspgrdom  16348  usgredg2en  16353  usgredgprv  16354  usgrpredgv  16356  usgredg  16358  usgrnloopv  16359  usgredgne  16362  usgredg3  16372  usgredgedg  16385  usgredgdomord  16388  usgr1vr  16406  subgruhgrfun  16426  subupgr  16431  subumgr  16432  subusgr  16433  umgrwlknloop  16526  wlkres  16537  clwwlkccatlem  16558  clwwlkccat  16559  depindlem1  16664  depindlem2  16665  depindlem3  16666  bj-inex  16850  bj-nn0suc  16907  bj-nn0sucALT  16921  trilpolemeq1  16997  trilpolemlt1  16998  trirec0  17001  nconstwlpolemgt0  17022