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  4167  otexg  4316  opelopabt  4350  sonr  4408  sotr  4409  issod  4410  so2nr  4412  so3nr  4413  ordelss  4470  onelon  4475  elrnmpt1s  4974  iota2  5308  funeu  5343  imadif  5401  fnbr  5425  feu  5508  f1ss  5537  f1ssres  5540  f1resf1  5541  dffo2  5552  foco  5559  foun  5591  fun11iun  5593  ffoss  5604  funbrfv  5670  fvco3  5705  fvopab6  5731  funfvbrb  5748  elpreima  5754  ffvelcdm  5768  ffvelcdmda  5770  dffo4  5783  fmptco  5801  fsn2  5809  fvconst2g  5853  fex  5868  funfvima  5871  f1elima  5897  f1ocnvfv1  5901  f1ocnvfv2  5902  cocan2  5912  foeqcnvco  5914  isocnv  5935  isores2  5937  isoini  5942  isoselem  5944  f1oiso  5950  f1ofveu  5989  eloprabga  6091  suppssof1  6236  ofco  6237  offveqb  6238  ofc1g  6240  ofc2g  6241  caofid0l  6245  caofid0r  6246  caofid1  6247  caofid2  6248  fnexALT  6256  f1dmex  6261  ot1stg  6298  ot2ndg  6299  ot3rdgg  6300  eqopi  6318  2ndrn  6329  fo2ndf  6373  smores3  6439  smores2  6440  smoel  6446  smoiso  6448  tfrlem1  6454  tfrlemisucaccv  6471  tfrlemibxssdm  6473  tfrlemiubacc  6476  tfr1onlemsucaccv  6487  tfr1onlembfn  6490  tfr1onlemubacc  6492  tfr1onlemaccex  6494  tfr1onlemres  6495  tfrcllemsucaccv  6500  tfrcllembfn  6503  tfrcllemubacc  6505  tfrcllemaccex  6507  tfrcllemres  6508  tfrcl  6510  frecrdg  6554  omv2  6611  nnasuc  6622  nnmsuc  6623  nnacom  6630  nnaass  6631  nnmass  6633  nntri1  6642  nndifsnid  6653  nnmordi  6662  swoer  6708  erth  6726  riinerm  6755  qliftlem  6760  ecovass  6791  ecoviass  6792  elmapssres  6820  fvixp  6850  f1domg  6909  domssr  6929  endomtr  6942  xpsnen2g  6988  enen1  7001  enen2  7002  domen1  7003  domen2  7004  mapen  7007  mapxpen  7009  ssenen  7012  phplem1  7013  fidifsnid  7033  findcard  7050  findcard2  7051  findcard2s  7052  fieq0  7143  isotilem  7173  supisolem  7175  inflbti  7191  ordiso2  7202  djuex  7210  updjudhcoinlf  7247  updjudhcoinrg  7248  updjud  7249  ctssdccl  7278  enumctlemm  7281  nnnninf  7293  finomni  7307  pm54.43  7363  acfun  7389  ccfunen  7450  cc2lem  7452  cc3  7454  addclpi  7514  addasspig  7517  mulasspig  7519  addnidpig  7523  nnppipi  7530  ltanqi  7589  ltmnqi  7590  ltexnqq  7595  archnqq  7604  prarloclemarch2  7606  enq0sym  7619  enq0tr  7621  nqnq0pi  7625  nqnq0  7628  mulcanenq0ec  7632  addclnq0  7638  nqpnq0nq  7640  distrnq0  7646  addassnq0lemcl  7648  addassnq0  7649  prubl  7673  prarloclemlt  7680  genpdf  7695  genipv  7696  genpelvl  7699  genpelvu  7700  genpml  7704  genpmu  7705  genprndl  7708  genprndu  7709  genpassl  7711  genpassu  7712  genpassg  7713  addnqprl  7716  addnqpru  7717  addlocpr  7723  nqprm  7729  nqprl  7738  nqpru  7739  mulnqprl  7755  mulnqpru  7756  mullocprlem  7757  mullocpr  7758  addcomprg  7765  mulcomprg  7767  distrlem1prl  7769  distrlem1pru  7770  distrlem4prl  7771  distrlem4pru  7772  ltprordil  7776  1idprl  7777  1idpru  7778  ltpopr  7782  ltsopr  7783  ltaddpr  7784  ltexprlemm  7787  ltexprlemopl  7788  ltexprlemlol  7789  ltexprlemopu  7790  ltexprlemupu  7791  ltexprlemdisj  7793  ltexprlemloc  7794  ltexprlemfl  7796  ltexprlemrl  7797  ltexprlemfu  7798  ltexprlemru  7799  addcanprleml  7801  addcanprlemu  7802  prplnqu  7807  recexprlemloc  7818  recexprlem1ssl  7820  recexprlem1ssu  7821  recexprlemss1l  7822  recexprlemss1u  7823  aptiprleml  7826  aptiprlemu  7827  cauappcvgprlemloc  7839  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  caucvgprlemloc  7862  caucvgprlemladdrl  7865  caucvgprprlemml  7881  caucvgprprlemloc  7890  00sr  7956  map2psrprg  7992  suplocsrlempr  7994  suplocsrlem  7995  adddir  8137  axsuploc  8219  eqle  8238  le2tri3i  8255  mul4  8278  muladd11  8279  cnegexlem3  8323  addsub12  8359  2addsub  8360  addsubeq4  8361  subadd4  8390  negcon1  8398  negdi2  8404  negsubdi2  8405  neg2sub  8406  renegcl  8407  muladd  8530  subdir  8532  gt0ne0  8574  ltnegcon1  8610  lenegcon1  8613  eqord1  8630  eqord2  8631  recexre  8725  ltmul1  8739  recexap  8800  div12ap  8841  rerecapb  8990  p1le  8996  ltmul2  9003  gt0div  9017  ge0div  9018  zlem1lt  9503  nnaddm1cl  9508  zdceq  9522  gtndiv  9542  prime  9546  msqznn  9547  btwnz  9566  uzss  9743  eluzadd  9751  nn0pzuz  9782  supinfneg  9790  infsupneg  9791  divfnzn  9816  qnegcl  9831  qreccl  9837  elpqb  9845  xaddass  10065  xleadd1a  10069  xlesubadd  10079  elico2  10133  iccss  10137  iccsupr  10162  elfz5  10213  fznn  10285  difelfznle  10331  fzoaddel  10393  elincfzoext  10399  qdceq  10464  qbtwnxr  10477  flqbi2  10511  adddivflid  10512  fldivnn0  10515  divfl0  10516  flqmulnn0  10519  fldivnn0le  10523  fldiv4p1lem1div2  10525  ceiqle  10535  flqdiv  10543  modqmulnn  10564  frecuzrdgtcl  10634  frecuzrdgsuc  10636  frecuzrdgdomlem  10639  frecuzrdgfunlem  10641  frecuzrdgsuctlem  10645  seqm1g  10696  seq3caopr2  10715  seqcaopr2g  10716  iseqf1olemkle  10719  seq3f1olemp  10737  seqf1oglem2  10742  seqf1og  10743  seq3id  10747  seq3z  10750  expap0  10791  mulexp  10800  mulexpzap  10801  expmul  10806  leexp1a  10816  expubnd  10818  zesq  10880  bernneq  10882  bernneq3  10884  modqexp  10888  facdiv  10960  facndiv  10961  faclbnd3  10965  faclbnd6  10966  bccmpl  10976  bcpasc  10988  bccl  10989  seq3coll  11064  fundm2domnop  11068  wrdsymb1  11108  ccatfv0  11138  ccatrn  11144  ccat2s1cl  11166  lswccats1fst  11175  swrdspsleq  11199  pfxtrcfv  11225  pfxsuffeqwrdeq  11230  pfxlswccat  11245  wrdeqs1cat  11252  cats1un  11253  swrdccatin1  11257  pfxccatin12lem4  11258  swrdccatin2  11261  pfxccatin12  11265  swrdccat  11267  shftlem  11327  ovshftex  11330  shftval4  11339  shftf  11341  shftcan2  11346  crim  11369  mulreap  11375  remul2  11384  immul2  11391  cjexp  11404  caucvgre  11492  r19.2uz  11504  sqrtsq2  11554  absnid  11584  absexp  11590  nn0abscl  11596  abslt  11599  lenegsq  11606  cau3lem  11625  minmax  11741  xrmaxadd  11772  clim  11792  climshftlemg  11813  climcn1  11819  climcn1lem  11830  clim2ser  11848  clim2ser2  11849  iserex  11850  isermulc2  11851  climub  11855  climcaucn  11862  serf0  11863  summodclem3  11891  summodclem2a  11892  summodclem2  11893  summodc  11894  fsum3  11898  fsumf1o  11901  fisumss  11903  isumss2  11904  fsumcl2lem  11909  fsumadd  11917  fsumsplit  11918  isummulc2  11937  fsum2d  11946  fsummulc2  11959  telfsumo  11977  fsumparts  11981  hash2iun1dif1  11991  bcxmas  12000  isumshft  12001  isumsplit  12002  expcnvap0  12013  geolim  12022  geolim2  12023  cvgratnnlemmn  12036  cvgratnnlemseq  12037  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  clim2divap  12051  prodmodclem3  12086  prodmodclem2a  12087  fprodseq  12094  fprodf1o  12099  fprodmul  12102  fprodsplitdc  12107  efcllemp  12169  reefcl  12179  efcj  12184  efaddlem  12185  efexp  12193  reeftlcl  12200  eftlub  12201  efsep  12202  effsumlt  12203  eflegeo  12212  retanclap  12233  demoivre  12284  demoivreALT  12285  eirraplem  12288  dvdsval3  12302  p1modz1  12305  iddvdsexp  12326  alzdvds  12365  addmodlteqALT  12370  nnehalf  12415  nno  12417  ndvdsadd  12442  bitsp1e  12463  bitsp1o  12464  bitsinv1  12473  divgcdnnr  12497  neggcd  12504  gcdabs  12509  bezoutlemmain  12519  bezoutlemaz  12524  bezoutlembz  12525  gcdmultiplez  12542  gcdzeq  12543  dvdssq  12552  nninfctlemfo  12561  algrf  12567  algcvg  12570  algcvga  12573  algfx  12574  eucalgf  12577  eucalgcvga  12580  neglcm  12597  lcmabs  12598  lcmdvds  12601  lcmgcdeq  12605  qredeq  12618  isprm3  12640  coprm  12666  prmrp  12667  isprm6  12669  prmdvdsexpb  12671  rpexp  12675  cncongrprm  12679  sqrt2irraplemnn  12701  phibndlem  12738  phiprmpw  12744  eulerthlemh  12753  eulerthlemth  12754  fermltl  12756  prmdivdiv  12759  modprm1div  12770  m1dvdsndvds  12771  coprimeprodsq  12780  pczpre  12820  pczcl  12821  pcexp  12832  pczdvds  12837  pczndvds  12839  pczndvds2  12841  pcdvdsb  12843  pcneg  12848  pcprmpw  12857  difsqpwdvds  12861  pcmptcl  12865  pcprod  12869  fldivp1  12871  infpnlem2  12883  1arithlem4  12889  ennnfonelemrn  12990  topnidg  13285  pwselbasb  13326  pwsplusgval  13328  pwsmulrval  13329  imasaddfnlemg  13347  imasaddflemg  13349  qusin  13359  mgmlrid  13412  mndass  13457  prdsidlem  13480  mhmco  13523  gsumsubm  13527  gsumwcl  13530  gsumwmhm  13531  grpass  13542  grpinvex  13543  dfgrp2  13560  grplid  13564  grprid  13565  grprcan  13570  grpinvssd  13610  grpinvval2  13616  prdsinvlem  13641  pwsinvg  13645  mhmid  13652  mhmmnd  13653  ghmgrp  13655  mulgnn  13663  mulgnnp1  13667  mulgnegnn  13669  mulgnnsubcl  13671  mulgz  13687  issubg2m  13726  issubg4m  13730  subgintm  13735  nmzbi  13746  eqger  13761  eqgid  13763  eqgen  13764  qusgrp  13769  qusadd  13771  qusinv  13773  qussub  13774  ghminv  13787  ghmsub  13788  ghmrn  13794  resghm2b  13799  ghmf1  13810  conjsubg  13814  conjsubgen  13815  qusghm  13819  cmncom  13839  ablsubadd  13849  ablsubsub23  13862  ghmcmn  13864  gsumfzreidx  13874  mgpress  13894  srg1expzeq1  13958  ringinvnz1ne0  14012  ringinvnzdiv  14013  dvdsrd  14058  dvdsunit  14076  unitinvcl  14087  unitinvinv  14088  unitlinv  14090  unitrinv  14091  rhmunitinv  14142  subrngintm  14176  subrg1  14195  subrguss  14200  subrginv  14201  subrgunit  14203  subrgugrp  14204  subrgintm  14207  resrhm  14212  resrhm2b  14213  lmodass  14267  lmodlcan  14268  lmod0vlid  14282  lmod0vrid  14283  lmod0vid  14284  lmodvs0  14286  lcomf  14291  lmodvnegcl  14292  lmodvnegid  14293  lmodvsubadd  14302  lmodsubid  14311  lss1d  14347  lspval  14354  lspsnel6  14372  lspsnneg  14384  sralmod  14414  dflidl2rng  14445  lidlacl  14448  dflidl2  14452  df2idl2  14473  qusmul2  14493  quscrng  14497  cnfldmulg  14540  znf1o  14615  znidom  14621  psraddcl  14644  psr0lid  14646  tgss3  14752  clsval  14785  clsss3  14804  neiss2  14816  resttop  14844  resttopon2  14852  lmconst  14890  cnima  14894  cnntri  14898  cncnp  14904  cnrest  14909  cndis  14915  lmss  14920  lmff  14923  lmtopcnp  14924  txcnp  14945  upxp  14946  uptx  14948  cnmpt11  14957  hmeoima  14984  hmeoopn  14985  hmeocld  14986  hmeontr  14987  hmeoimaf1o  14988  mettri2  15036  met0  15038  metres2  15055  blpnf  15074  xblss2ps  15078  xblss2  15079  blbas  15107  blres  15108  xmetec  15111  mopnss  15124  xmstri2  15144  mstri2  15145  xmstri  15146  mstri  15147  xmstri3  15148  mstri3  15149  msrtri  15150  mopni3  15158  unimopn  15160  comet  15173  bdxmet  15175  climcncf  15258  dedekindeulemuub  15291  dedekindicclemuub  15300  ivthdichlem  15325  dvfgg  15362  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvfre  15384  dvmptfsum  15399  plyadd  15425  plymul  15426  reeff1olem  15445  reeff1o  15447  sinperlem  15482  abssinper  15520  reexplog  15545  relogexp  15546  cxpexpnn  15570  cxprec  15584  rpcxpmul2  15587  abscxp  15589  wilthlem1  15654  sgmval2  15658  sgmnncl  15662  0sgmppw  15667  perfectlem1  15673  lgsdir  15714  lgsprme0  15721  lgsdinn0  15727  gausslemma2dlem3  15742  gausslemma2dlem5a  15744  2lgslem1a2  15766  2lgslem1a  15767  2lgslem3  15780  2lgs  15783  umgredgprv  15915  umgrislfupgrdom  15929  uspgredgiedg  15976  uspgriedgedg  15977  usgrislfuspgrdom  15988  usgredg2en  15993  usgredgprv  15994  usgrpredgv  15996  usgredg  15998  usgrnloopv  15999  usgredgne  16002  usgredg3  16012  usgredgedg  16025  usgredgdomord  16028  umgrwlknloop  16079  bj-inex  16270  bj-nn0suc  16327  bj-nn0sucALT  16341  trilpolemeq1  16408  trilpolemlt1  16409  trirec0  16412  nconstwlpolemgt0  16432