Theorem sylan 281

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 115	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	mpan9 279	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  sylanb  282  sylanbr  283  syl2an  287  sylanl1  400  sylanl2  401  mpanl1  432  mpanl2  433  adantll  473  adantlr  474  ancom1s  564  3adantl1  1148  3adantl2  1149  3adantl3  1150  syl3anl1  1281  syl3anl3  1283  syl3anl  1284  stoic3  1424  eupick  2098  csbiebt  3088  csbnestgf  3101  reuss2  3407  mpteq12  4070  otexg  4213  opelopabt  4245  sonr  4300  sotr  4301  issod  4302  so2nr  4304  so3nr  4305  ordelss  4362  onelon  4367  elrnmpt1s  4859  iota2  5186  funeu  5221  imadif  5276  fnbr  5298  feu  5378  f1ss  5407  f1ssres  5410  f1resf1  5411  dffo2  5422  foco  5428  foun  5459  fun11iun  5461  ffoss  5472  funbrfv  5533  fvco3  5565  fvopab6  5590  funfvbrb  5606  elpreima  5612  ffvelrn  5626  ffvelrnda  5628  dffo4  5641  fmptco  5659  fsn2  5667  fvconst2g  5707  fex  5722  funfvima  5724  f1elima  5749  f1ocnvfv1  5753  f1ocnvfv2  5754  cocan2  5764  foeqcnvco  5766  isocnv  5787  isores2  5789  isoini  5794  isoselem  5796  f1oiso  5802  f1ofveu  5838  eloprabga  5937  suppssof1  6075  ofco  6076  offveqb  6077  fnexALT  6087  f1dmex  6092  ot1stg  6128  ot2ndg  6129  ot3rdgg  6130  eqopi  6148  2ndrn  6159  fo2ndf  6203  smores3  6269  smores2  6270  smoel  6276  smoiso  6278  tfrlem1  6284  tfrlemisucaccv  6301  tfrlemibxssdm  6303  tfrlemiubacc  6306  tfr1onlemsucaccv  6317  tfr1onlembfn  6320  tfr1onlemubacc  6322  tfr1onlemaccex  6324  tfr1onlemres  6325  tfrcllemsucaccv  6330  tfrcllembfn  6333  tfrcllemubacc  6335  tfrcllemaccex  6337  tfrcllemres  6338  tfrcl  6340  frecrdg  6384  omv2  6441  nnasuc  6452  nnmsuc  6453  nnacom  6460  nnaass  6461  nnmass  6463  nntri1  6472  nndifsnid  6483  nnmordi  6492  swoer  6537  erth  6553  riinerm  6582  qliftlem  6587  ecovass  6618  ecoviass  6619  elmapssres  6647  fvixp  6677  f1domg  6732  endomtr  6764  xpsnen2g  6803  enen1  6814  enen2  6815  domen1  6816  domen2  6817  mapen  6820  mapxpen  6822  ssenen  6825  phplem1  6826  fidifsnid  6845  findcard  6862  findcard2  6863  findcard2s  6864  fieq0  6949  isotilem  6979  supisolem  6981  inflbti  6997  ordiso2  7008  djuex  7016  updjudhcoinlf  7053  updjudhcoinrg  7054  updjud  7055  ctssdccl  7084  enumctlemm  7087  nnnninf  7098  finomni  7112  pm54.43  7154  acfun  7171  ccfunen  7213  cc2lem  7215  cc3  7217  addclpi  7276  addasspig  7279  mulasspig  7281  addnidpig  7285  nnppipi  7292  ltanqi  7351  ltmnqi  7352  ltexnqq  7357  archnqq  7366  prarloclemarch2  7368  enq0sym  7381  enq0tr  7383  nqnq0pi  7387  nqnq0  7390  mulcanenq0ec  7394  addclnq0  7400  nqpnq0nq  7402  distrnq0  7408  addassnq0lemcl  7410  addassnq0  7411  prubl  7435  prarloclemlt  7442  genpdf  7457  genipv  7458  genpelvl  7461  genpelvu  7462  genpml  7466  genpmu  7467  genprndl  7470  genprndu  7471  genpassl  7473  genpassu  7474  genpassg  7475  addnqprl  7478  addnqpru  7479  addlocpr  7485  nqprm  7491  nqprl  7500  nqpru  7501  mulnqprl  7517  mulnqpru  7518  mullocprlem  7519  mullocpr  7520  addcomprg  7527  mulcomprg  7529  distrlem1prl  7531  distrlem1pru  7532  distrlem4prl  7533  distrlem4pru  7534  ltprordil  7538  1idprl  7539  1idpru  7540  ltpopr  7544  ltsopr  7545  ltaddpr  7546  ltexprlemm  7549  ltexprlemopl  7550  ltexprlemlol  7551  ltexprlemopu  7552  ltexprlemupu  7553  ltexprlemdisj  7555  ltexprlemloc  7556  ltexprlemfl  7558  ltexprlemrl  7559  ltexprlemfu  7560  ltexprlemru  7561  addcanprleml  7563  addcanprlemu  7564  prplnqu  7569  recexprlemloc  7580  recexprlem1ssl  7582  recexprlem1ssu  7583  recexprlemss1l  7584  recexprlemss1u  7585  aptiprleml  7588  aptiprlemu  7589  cauappcvgprlemloc  7601  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  caucvgprlemloc  7624  caucvgprlemladdrl  7627  caucvgprprlemml  7643  caucvgprprlemloc  7652  00sr  7718  map2psrprg  7754  suplocsrlempr  7756  suplocsrlem  7757  adddir  7898  axsuploc  7979  eqle  7998  le2tri3i  8015  mul4  8038  muladd11  8039  cnegexlem3  8083  addsub12  8119  2addsub  8120  addsubeq4  8121  subadd4  8150  negcon1  8158  negdi2  8164  negsubdi2  8165  neg2sub  8166  renegcl  8167  muladd  8290  subdir  8292  gt0ne0  8333  ltnegcon1  8369  lenegcon1  8372  eqord1  8389  eqord2  8390  recexre  8484  ltmul1  8498  recexap  8558  div12ap  8598  p1le  8752  ltmul2  8759  gt0div  8773  ge0div  8774  zlem1lt  9255  nnaddm1cl  9260  zdceq  9274  gtndiv  9294  prime  9298  msqznn  9299  btwnz  9318  uzss  9494  eluzadd  9502  nn0pzuz  9533  supinfneg  9541  infsupneg  9542  divfnzn  9567  qnegcl  9582  qreccl  9588  elpqb  9595  xaddass  9813  xleadd1a  9817  xlesubadd  9827  elico2  9881  iccss  9885  iccsupr  9910  elfz5  9960  fznn  10032  difelfznle  10078  fzoaddel  10135  qdceq  10190  qbtwnxr  10201  flqbi2  10234  adddivflid  10235  fldivnn0  10238  divfl0  10239  flqmulnn0  10242  fldivnn0le  10246  fldiv4p1lem1div2  10248  ceiqle  10256  flqdiv  10264  modqmulnn  10285  frecuzrdgtcl  10355  frecuzrdgsuc  10357  frecuzrdgdomlem  10360  frecuzrdgfunlem  10362  frecuzrdgsuctlem  10366  seq3caopr2  10425  iseqf1olemkle  10427  seq3f1olemp  10445  seq3id  10451  seq3z  10454  expap0  10493  mulexp  10502  mulexpzap  10503  expmul  10508  leexp1a  10518  expubnd  10520  zesq  10581  bernneq  10583  bernneq3  10585  modqexp  10589  facdiv  10659  facndiv  10660  faclbnd3  10664  faclbnd6  10665  bccmpl  10675  bcpasc  10687  bccl  10688  seq3coll  10764  shftlem  10767  ovshftex  10770  shftval4  10779  shftf  10781  shftcan2  10786  crim  10809  mulreap  10815  remul2  10824  immul2  10831  cjexp  10844  caucvgre  10932  r19.2uz  10944  sqrtsq2  10994  absnid  11024  absexp  11030  nn0abscl  11036  abslt  11039  lenegsq  11046  cau3lem  11065  minmax  11180  xrmaxadd  11211  clim  11231  climshftlemg  11252  climcn1  11258  climcn1lem  11269  clim2ser  11287  clim2ser2  11288  iserex  11289  isermulc2  11290  climub  11294  climcaucn  11301  serf0  11302  summodclem3  11330  summodclem2a  11331  summodclem2  11332  summodc  11333  fsum3  11337  fsumf1o  11340  fisumss  11342  isumss2  11343  fsumcl2lem  11348  fsumadd  11356  fsumsplit  11357  isummulc2  11376  fsum2d  11385  fsummulc2  11398  telfsumo  11416  fsumparts  11420  hash2iun1dif1  11430  bcxmas  11439  isumshft  11440  isumsplit  11441  expcnvap0  11452  geolim  11461  geolim2  11462  cvgratnnlemmn  11475  cvgratnnlemseq  11476  mertenslemi1  11485  mertenslem2  11486  mertensabs  11487  clim2divap  11490  prodmodclem3  11525  prodmodclem2a  11526  fprodseq  11533  fprodf1o  11538  fprodmul  11541  fprodsplitdc  11546  efcllemp  11608  reefcl  11618  efcj  11623  efaddlem  11624  efexp  11632  reeftlcl  11639  eftlub  11640  efsep  11641  effsumlt  11642  eflegeo  11651  retanclap  11672  demoivre  11722  demoivreALT  11723  eirraplem  11726  dvdsval3  11740  p1modz1  11743  iddvdsexp  11764  alzdvds  11801  addmodlteqALT  11806  nnehalf  11850  nno  11852  ndvdsadd  11877  divgcdnnr  11918  neggcd  11925  gcdabs  11930  bezoutlemmain  11940  bezoutlemaz  11945  bezoutlembz  11946  gcdmultiplez  11963  gcdzeq  11964  dvdssq  11973  algrf  11986  algcvg  11989  algcvga  11992  algfx  11993  eucalgf  11996  eucalgcvga  11999  neglcm  12016  lcmabs  12017  lcmdvds  12020  lcmgcdeq  12024  qredeq  12037  isprm3  12059  coprm  12085  prmrp  12086  isprm6  12088  prmdvdsexpb  12090  rpexp  12094  cncongrprm  12098  sqrt2irraplemnn  12120  phibndlem  12157  phiprmpw  12163  eulerthlemh  12172  eulerthlemth  12173  fermltl  12175  prmdivdiv  12178  modprm1div  12188  m1dvdsndvds  12189  coprimeprodsq  12198  pczpre  12238  pczcl  12239  pcexp  12250  pczdvds  12254  pczndvds  12256  pczndvds2  12258  pcdvdsb  12260  pcneg  12265  pcprmpw  12274  difsqpwdvds  12278  pcmptcl  12281  pcprod  12285  fldivp1  12287  infpnlem2  12299  1arithlem4  12305  ennnfonelemrn  12361  topnidg  12579  mgmlrid  12620  mndass  12647  mhmco  12692  grpass  12704  grpinvex  12705  dfgrp2  12719  grplid  12723  grprid  12724  grprcan  12727  tgss3  12831  clsval  12864  clsss3  12883  neiss2  12895  resttop  12923  resttopon2  12931  lmconst  12969  cnima  12973  cnntri  12977  cncnp  12983  cnrest  12988  cndis  12994  lmss  12999  lmff  13002  lmtopcnp  13003  txcnp  13024  upxp  13025  uptx  13027  cnmpt11  13036  hmeoima  13063  hmeoopn  13064  hmeocld  13065  hmeontr  13066  hmeoimaf1o  13067  mettri2  13115  met0  13117  metres2  13134  blpnf  13153  xblss2ps  13157  xblss2  13158  blbas  13186  blres  13187  xmetec  13190  mopnss  13203  xmstri2  13223  mstri2  13224  xmstri  13225  mstri  13226  xmstri3  13227  mstri3  13228  msrtri  13229  mopni3  13237  unimopn  13239  comet  13252  bdxmet  13254  climcncf  13324  dedekindeulemuub  13348  dedekindicclemuub  13357  dvfgg  13410  dvidlemap  13413  dvfre  13427  reeff1olem  13445  reeff1o  13447  sinperlem  13482  abssinper  13520  reexplog  13545  relogexp  13546  cxpexpnn  13570  cxprec  13584  abscxp  13588  lgsdir  13689  lgsprme0  13696  lgsdinn0  13702  bj-inex  13902  bj-nn0suc  13959  bj-nn0sucALT  13973  trilpolemeq1  14032  trilpolemlt1  14033  trirec0  14036  nconstwlpolemgt0  14055