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  3adantl1  1153  3adantl2  1154  3adantl3  1155  syl3anl1  1286  syl3anl3  1288  syl3anl  1289  stoic3  1431  eupick  2105  csbiebt  3097  csbnestgf  3110  reuss2  3416  mpteq12  4087  otexg  4231  opelopabt  4263  sonr  4318  sotr  4319  issod  4320  so2nr  4322  so3nr  4323  ordelss  4380  onelon  4385  elrnmpt1s  4878  iota2  5207  funeu  5242  imadif  5297  fnbr  5319  feu  5399  f1ss  5428  f1ssres  5431  f1resf1  5432  dffo2  5443  foco  5449  foun  5481  fun11iun  5483  ffoss  5494  funbrfv  5555  fvco3  5588  fvopab6  5613  funfvbrb  5630  elpreima  5636  ffvelcdm  5650  ffvelcdmda  5652  dffo4  5665  fmptco  5683  fsn2  5691  fvconst2g  5731  fex  5746  funfvima  5749  f1elima  5774  f1ocnvfv1  5778  f1ocnvfv2  5779  cocan2  5789  foeqcnvco  5791  isocnv  5812  isores2  5814  isoini  5819  isoselem  5821  f1oiso  5827  f1ofveu  5863  eloprabga  5962  suppssof1  6100  ofco  6101  offveqb  6102  fnexALT  6112  f1dmex  6117  ot1stg  6153  ot2ndg  6154  ot3rdgg  6155  eqopi  6173  2ndrn  6184  fo2ndf  6228  smores3  6294  smores2  6295  smoel  6301  smoiso  6303  tfrlem1  6309  tfrlemisucaccv  6326  tfrlemibxssdm  6328  tfrlemiubacc  6331  tfr1onlemsucaccv  6342  tfr1onlembfn  6345  tfr1onlemubacc  6347  tfr1onlemaccex  6349  tfr1onlemres  6350  tfrcllemsucaccv  6355  tfrcllembfn  6358  tfrcllemubacc  6360  tfrcllemaccex  6362  tfrcllemres  6363  tfrcl  6365  frecrdg  6409  omv2  6466  nnasuc  6477  nnmsuc  6478  nnacom  6485  nnaass  6486  nnmass  6488  nntri1  6497  nndifsnid  6508  nnmordi  6517  swoer  6563  erth  6579  riinerm  6608  qliftlem  6613  ecovass  6644  ecoviass  6645  elmapssres  6673  fvixp  6703  f1domg  6758  endomtr  6790  xpsnen2g  6829  enen1  6840  enen2  6841  domen1  6842  domen2  6843  mapen  6846  mapxpen  6848  ssenen  6851  phplem1  6852  fidifsnid  6871  findcard  6888  findcard2  6889  findcard2s  6890  fieq0  6975  isotilem  7005  supisolem  7007  inflbti  7023  ordiso2  7034  djuex  7042  updjudhcoinlf  7079  updjudhcoinrg  7080  updjud  7081  ctssdccl  7110  enumctlemm  7113  nnnninf  7124  finomni  7138  pm54.43  7189  acfun  7206  ccfunen  7263  cc2lem  7265  cc3  7267  addclpi  7326  addasspig  7329  mulasspig  7331  addnidpig  7335  nnppipi  7342  ltanqi  7401  ltmnqi  7402  ltexnqq  7407  archnqq  7416  prarloclemarch2  7418  enq0sym  7431  enq0tr  7433  nqnq0pi  7437  nqnq0  7440  mulcanenq0ec  7444  addclnq0  7450  nqpnq0nq  7452  distrnq0  7458  addassnq0lemcl  7460  addassnq0  7461  prubl  7485  prarloclemlt  7492  genpdf  7507  genipv  7508  genpelvl  7511  genpelvu  7512  genpml  7516  genpmu  7517  genprndl  7520  genprndu  7521  genpassl  7523  genpassu  7524  genpassg  7525  addnqprl  7528  addnqpru  7529  addlocpr  7535  nqprm  7541  nqprl  7550  nqpru  7551  mulnqprl  7567  mulnqpru  7568  mullocprlem  7569  mullocpr  7570  addcomprg  7577  mulcomprg  7579  distrlem1prl  7581  distrlem1pru  7582  distrlem4prl  7583  distrlem4pru  7584  ltprordil  7588  1idprl  7589  1idpru  7590  ltpopr  7594  ltsopr  7595  ltaddpr  7596  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemfl  7608  ltexprlemrl  7609  ltexprlemfu  7610  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  prplnqu  7619  recexprlemloc  7630  recexprlem1ssl  7632  recexprlem1ssu  7633  recexprlemss1l  7634  recexprlemss1u  7635  aptiprleml  7638  aptiprlemu  7639  cauappcvgprlemloc  7651  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemloc  7674  caucvgprlemladdrl  7677  caucvgprprlemml  7693  caucvgprprlemloc  7702  00sr  7768  map2psrprg  7804  suplocsrlempr  7806  suplocsrlem  7807  adddir  7948  axsuploc  8030  eqle  8049  le2tri3i  8066  mul4  8089  muladd11  8090  cnegexlem3  8134  addsub12  8170  2addsub  8171  addsubeq4  8172  subadd4  8201  negcon1  8209  negdi2  8215  negsubdi2  8216  neg2sub  8217  renegcl  8218  muladd  8341  subdir  8343  gt0ne0  8384  ltnegcon1  8420  lenegcon1  8423  eqord1  8440  eqord2  8441  recexre  8535  ltmul1  8549  recexap  8610  div12ap  8651  rerecapb  8800  p1le  8806  ltmul2  8813  gt0div  8827  ge0div  8828  zlem1lt  9309  nnaddm1cl  9314  zdceq  9328  gtndiv  9348  prime  9352  msqznn  9353  btwnz  9372  uzss  9548  eluzadd  9556  nn0pzuz  9587  supinfneg  9595  infsupneg  9596  divfnzn  9621  qnegcl  9636  qreccl  9642  elpqb  9649  xaddass  9869  xleadd1a  9873  xlesubadd  9883  elico2  9937  iccss  9941  iccsupr  9966  elfz5  10017  fznn  10089  difelfznle  10135  fzoaddel  10192  qdceq  10247  qbtwnxr  10258  flqbi2  10291  adddivflid  10292  fldivnn0  10295  divfl0  10296  flqmulnn0  10299  fldivnn0le  10303  fldiv4p1lem1div2  10305  ceiqle  10313  flqdiv  10321  modqmulnn  10342  frecuzrdgtcl  10412  frecuzrdgsuc  10414  frecuzrdgdomlem  10417  frecuzrdgfunlem  10419  frecuzrdgsuctlem  10423  seq3caopr2  10482  iseqf1olemkle  10484  seq3f1olemp  10502  seq3id  10508  seq3z  10511  expap0  10550  mulexp  10559  mulexpzap  10560  expmul  10565  leexp1a  10575  expubnd  10577  zesq  10639  bernneq  10641  bernneq3  10643  modqexp  10647  facdiv  10718  facndiv  10719  faclbnd3  10723  faclbnd6  10724  bccmpl  10734  bcpasc  10746  bccl  10747  seq3coll  10822  shftlem  10825  ovshftex  10828  shftval4  10837  shftf  10839  shftcan2  10844  crim  10867  mulreap  10873  remul2  10882  immul2  10889  cjexp  10902  caucvgre  10990  r19.2uz  11002  sqrtsq2  11052  absnid  11082  absexp  11088  nn0abscl  11094  abslt  11097  lenegsq  11104  cau3lem  11123  minmax  11238  xrmaxadd  11269  clim  11289  climshftlemg  11310  climcn1  11316  climcn1lem  11327  clim2ser  11345  clim2ser2  11346  iserex  11347  isermulc2  11348  climub  11352  climcaucn  11359  serf0  11360  summodclem3  11388  summodclem2a  11389  summodclem2  11390  summodc  11391  fsum3  11395  fsumf1o  11398  fisumss  11400  isumss2  11401  fsumcl2lem  11406  fsumadd  11414  fsumsplit  11415  isummulc2  11434  fsum2d  11443  fsummulc2  11456  telfsumo  11474  fsumparts  11478  hash2iun1dif1  11488  bcxmas  11497  isumshft  11498  isumsplit  11499  expcnvap0  11510  geolim  11519  geolim2  11520  cvgratnnlemmn  11533  cvgratnnlemseq  11534  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  clim2divap  11548  prodmodclem3  11583  prodmodclem2a  11584  fprodseq  11591  fprodf1o  11596  fprodmul  11599  fprodsplitdc  11604  efcllemp  11666  reefcl  11676  efcj  11681  efaddlem  11682  efexp  11690  reeftlcl  11697  eftlub  11698  efsep  11699  effsumlt  11700  eflegeo  11709  retanclap  11730  demoivre  11780  demoivreALT  11781  eirraplem  11784  dvdsval3  11798  p1modz1  11801  iddvdsexp  11822  alzdvds  11860  addmodlteqALT  11865  nnehalf  11909  nno  11911  ndvdsadd  11936  divgcdnnr  11977  neggcd  11984  gcdabs  11989  bezoutlemmain  11999  bezoutlemaz  12004  bezoutlembz  12005  gcdmultiplez  12022  gcdzeq  12023  dvdssq  12032  algrf  12045  algcvg  12048  algcvga  12051  algfx  12052  eucalgf  12055  eucalgcvga  12058  neglcm  12075  lcmabs  12076  lcmdvds  12079  lcmgcdeq  12083  qredeq  12096  isprm3  12118  coprm  12144  prmrp  12145  isprm6  12147  prmdvdsexpb  12149  rpexp  12153  cncongrprm  12157  sqrt2irraplemnn  12179  phibndlem  12216  phiprmpw  12222  eulerthlemh  12231  eulerthlemth  12232  fermltl  12234  prmdivdiv  12237  modprm1div  12247  m1dvdsndvds  12248  coprimeprodsq  12257  pczpre  12297  pczcl  12298  pcexp  12309  pczdvds  12313  pczndvds  12315  pczndvds2  12317  pcdvdsb  12319  pcneg  12324  pcprmpw  12333  difsqpwdvds  12337  pcmptcl  12340  pcprod  12344  fldivp1  12346  infpnlem2  12358  1arithlem4  12364  ennnfonelemrn  12420  topnidg  12701  imasaddfnlemg  12735  imasaddflemg  12737  qusin  12746  mgmlrid  12798  mndass  12825  mhmco  12874  grpass  12886  grpinvex  12887  dfgrp2  12902  grplid  12906  grprid  12907  grprcan  12910  grpinvssd  12947  grpinvval2  12953  mhmid  12979  mhmmnd  12980  ghmgrp  12982  mulgnn  12989  mulgnnp1  12991  mulgnegnn  12993  mulgnnsubcl  12995  mulgz  13011  issubg2m  13049  issubg4m  13053  subgintm  13058  nmzbi  13069  eqger  13083  eqgid  13085  eqgen  13086  cmncom  13105  ablsubadd  13115  ablsubsub23  13128  mgpress  13141  srg1expzeq1  13178  ringinvnz1ne0  13226  ringinvnzdiv  13227  dvdsrd  13263  dvdsunit  13281  unitinvcl  13292  unitinvinv  13293  unitlinv  13295  unitrinv  13296  subrg1  13352  subrguss  13357  subrginv  13358  subrgunit  13360  subrgugrp  13361  subrgintm  13364  lmodass  13393  lmodlcan  13394  lmod0vlid  13408  lmod0vrid  13409  lmod0vid  13410  lmodvs0  13412  lcomf  13417  lmodvnegcl  13418  lmodvnegid  13419  lmodvsubadd  13428  lmodsubid  13437  cnfldmulg  13473  tgss3  13581  clsval  13614  clsss3  13633  neiss2  13645  resttop  13673  resttopon2  13681  lmconst  13719  cnima  13723  cnntri  13727  cncnp  13733  cnrest  13738  cndis  13744  lmss  13749  lmff  13752  lmtopcnp  13753  txcnp  13774  upxp  13775  uptx  13777  cnmpt11  13786  hmeoima  13813  hmeoopn  13814  hmeocld  13815  hmeontr  13816  hmeoimaf1o  13817  mettri2  13865  met0  13867  metres2  13884  blpnf  13903  xblss2ps  13907  xblss2  13908  blbas  13936  blres  13937  xmetec  13940  mopnss  13953  xmstri2  13973  mstri2  13974  xmstri  13975  mstri  13976  xmstri3  13977  mstri3  13978  msrtri  13979  mopni3  13987  unimopn  13989  comet  14002  bdxmet  14004  climcncf  14074  dedekindeulemuub  14098  dedekindicclemuub  14107  dvfgg  14160  dvidlemap  14163  dvfre  14177  reeff1olem  14195  reeff1o  14197  sinperlem  14232  abssinper  14270  reexplog  14295  relogexp  14296  cxpexpnn  14320  cxprec  14334  abscxp  14338  lgsdir  14439  lgsprme0  14446  lgsdinn0  14452  bj-inex  14662  bj-nn0suc  14719  bj-nn0sucALT  14733  trilpolemeq1  14791  trilpolemlt1  14792  trirec0  14795  nconstwlpolemgt0  14814