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  4072  otexg  4215  opelopabt  4247  sonr  4302  sotr  4303  issod  4304  so2nr  4306  so3nr  4307  ordelss  4364  onelon  4369  elrnmpt1s  4861  iota2  5188  funeu  5223  imadif  5278  fnbr  5300  feu  5380  f1ss  5409  f1ssres  5412  f1resf1  5413  dffo2  5424  foco  5430  foun  5461  fun11iun  5463  ffoss  5474  funbrfv  5535  fvco3  5567  fvopab6  5592  funfvbrb  5609  elpreima  5615  ffvelrn  5629  ffvelrnda  5631  dffo4  5644  fmptco  5662  fsn2  5670  fvconst2g  5710  fex  5725  funfvima  5727  f1elima  5752  f1ocnvfv1  5756  f1ocnvfv2  5757  cocan2  5767  foeqcnvco  5769  isocnv  5790  isores2  5792  isoini  5797  isoselem  5799  f1oiso  5805  f1ofveu  5841  eloprabga  5940  suppssof1  6078  ofco  6079  offveqb  6080  fnexALT  6090  f1dmex  6095  ot1stg  6131  ot2ndg  6132  ot3rdgg  6133  eqopi  6151  2ndrn  6162  fo2ndf  6206  smores3  6272  smores2  6273  smoel  6279  smoiso  6281  tfrlem1  6287  tfrlemisucaccv  6304  tfrlemibxssdm  6306  tfrlemiubacc  6309  tfr1onlemsucaccv  6320  tfr1onlembfn  6323  tfr1onlemubacc  6325  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllemsucaccv  6333  tfrcllembfn  6336  tfrcllemubacc  6338  tfrcllemaccex  6340  tfrcllemres  6341  tfrcl  6343  frecrdg  6387  omv2  6444  nnasuc  6455  nnmsuc  6456  nnacom  6463  nnaass  6464  nnmass  6466  nntri1  6475  nndifsnid  6486  nnmordi  6495  swoer  6541  erth  6557  riinerm  6586  qliftlem  6591  ecovass  6622  ecoviass  6623  elmapssres  6651  fvixp  6681  f1domg  6736  endomtr  6768  xpsnen2g  6807  enen1  6818  enen2  6819  domen1  6820  domen2  6821  mapen  6824  mapxpen  6826  ssenen  6829  phplem1  6830  fidifsnid  6849  findcard  6866  findcard2  6867  findcard2s  6868  fieq0  6953  isotilem  6983  supisolem  6985  inflbti  7001  ordiso2  7012  djuex  7020  updjudhcoinlf  7057  updjudhcoinrg  7058  updjud  7059  ctssdccl  7088  enumctlemm  7091  nnnninf  7102  finomni  7116  pm54.43  7167  acfun  7184  ccfunen  7226  cc2lem  7228  cc3  7230  addclpi  7289  addasspig  7292  mulasspig  7294  addnidpig  7298  nnppipi  7305  ltanqi  7364  ltmnqi  7365  ltexnqq  7370  archnqq  7379  prarloclemarch2  7381  enq0sym  7394  enq0tr  7396  nqnq0pi  7400  nqnq0  7403  mulcanenq0ec  7407  addclnq0  7413  nqpnq0nq  7415  distrnq0  7421  addassnq0lemcl  7423  addassnq0  7424  prubl  7448  prarloclemlt  7455  genpdf  7470  genipv  7471  genpelvl  7474  genpelvu  7475  genpml  7479  genpmu  7480  genprndl  7483  genprndu  7484  genpassl  7486  genpassu  7487  genpassg  7488  addnqprl  7491  addnqpru  7492  addlocpr  7498  nqprm  7504  nqprl  7513  nqpru  7514  mulnqprl  7530  mulnqpru  7531  mullocprlem  7532  mullocpr  7533  addcomprg  7540  mulcomprg  7542  distrlem1prl  7544  distrlem1pru  7545  distrlem4prl  7546  distrlem4pru  7547  ltprordil  7551  1idprl  7552  1idpru  7553  ltpopr  7557  ltsopr  7558  ltaddpr  7559  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  prplnqu  7582  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  recexprlemss1l  7597  recexprlemss1u  7598  aptiprleml  7601  aptiprlemu  7602  cauappcvgprlemloc  7614  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemloc  7637  caucvgprlemladdrl  7640  caucvgprprlemml  7656  caucvgprprlemloc  7665  00sr  7731  map2psrprg  7767  suplocsrlempr  7769  suplocsrlem  7770  adddir  7911  axsuploc  7992  eqle  8011  le2tri3i  8028  mul4  8051  muladd11  8052  cnegexlem3  8096  addsub12  8132  2addsub  8133  addsubeq4  8134  subadd4  8163  negcon1  8171  negdi2  8177  negsubdi2  8178  neg2sub  8179  renegcl  8180  muladd  8303  subdir  8305  gt0ne0  8346  ltnegcon1  8382  lenegcon1  8385  eqord1  8402  eqord2  8403  recexre  8497  ltmul1  8511  recexap  8571  div12ap  8611  p1le  8765  ltmul2  8772  gt0div  8786  ge0div  8787  zlem1lt  9268  nnaddm1cl  9273  zdceq  9287  gtndiv  9307  prime  9311  msqznn  9312  btwnz  9331  uzss  9507  eluzadd  9515  nn0pzuz  9546  supinfneg  9554  infsupneg  9555  divfnzn  9580  qnegcl  9595  qreccl  9601  elpqb  9608  xaddass  9826  xleadd1a  9830  xlesubadd  9840  elico2  9894  iccss  9898  iccsupr  9923  elfz5  9973  fznn  10045  difelfznle  10091  fzoaddel  10148  qdceq  10203  qbtwnxr  10214  flqbi2  10247  adddivflid  10248  fldivnn0  10251  divfl0  10252  flqmulnn0  10255  fldivnn0le  10259  fldiv4p1lem1div2  10261  ceiqle  10269  flqdiv  10277  modqmulnn  10298  frecuzrdgtcl  10368  frecuzrdgsuc  10370  frecuzrdgdomlem  10373  frecuzrdgfunlem  10375  frecuzrdgsuctlem  10379  seq3caopr2  10438  iseqf1olemkle  10440  seq3f1olemp  10458  seq3id  10464  seq3z  10467  expap0  10506  mulexp  10515  mulexpzap  10516  expmul  10521  leexp1a  10531  expubnd  10533  zesq  10594  bernneq  10596  bernneq3  10598  modqexp  10602  facdiv  10672  facndiv  10673  faclbnd3  10677  faclbnd6  10678  bccmpl  10688  bcpasc  10700  bccl  10701  seq3coll  10777  shftlem  10780  ovshftex  10783  shftval4  10792  shftf  10794  shftcan2  10799  crim  10822  mulreap  10828  remul2  10837  immul2  10844  cjexp  10857  caucvgre  10945  r19.2uz  10957  sqrtsq2  11007  absnid  11037  absexp  11043  nn0abscl  11049  abslt  11052  lenegsq  11059  cau3lem  11078  minmax  11193  xrmaxadd  11224  clim  11244  climshftlemg  11265  climcn1  11271  climcn1lem  11282  clim2ser  11300  clim2ser2  11301  iserex  11302  isermulc2  11303  climub  11307  climcaucn  11314  serf0  11315  summodclem3  11343  summodclem2a  11344  summodclem2  11345  summodc  11346  fsum3  11350  fsumf1o  11353  fisumss  11355  isumss2  11356  fsumcl2lem  11361  fsumadd  11369  fsumsplit  11370  isummulc2  11389  fsum2d  11398  fsummulc2  11411  telfsumo  11429  fsumparts  11433  hash2iun1dif1  11443  bcxmas  11452  isumshft  11453  isumsplit  11454  expcnvap0  11465  geolim  11474  geolim2  11475  cvgratnnlemmn  11488  cvgratnnlemseq  11489  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  clim2divap  11503  prodmodclem3  11538  prodmodclem2a  11539  fprodseq  11546  fprodf1o  11551  fprodmul  11554  fprodsplitdc  11559  efcllemp  11621  reefcl  11631  efcj  11636  efaddlem  11637  efexp  11645  reeftlcl  11652  eftlub  11653  efsep  11654  effsumlt  11655  eflegeo  11664  retanclap  11685  demoivre  11735  demoivreALT  11736  eirraplem  11739  dvdsval3  11753  p1modz1  11756  iddvdsexp  11777  alzdvds  11814  addmodlteqALT  11819  nnehalf  11863  nno  11865  ndvdsadd  11890  divgcdnnr  11931  neggcd  11938  gcdabs  11943  bezoutlemmain  11953  bezoutlemaz  11958  bezoutlembz  11959  gcdmultiplez  11976  gcdzeq  11977  dvdssq  11986  algrf  11999  algcvg  12002  algcvga  12005  algfx  12006  eucalgf  12009  eucalgcvga  12012  neglcm  12029  lcmabs  12030  lcmdvds  12033  lcmgcdeq  12037  qredeq  12050  isprm3  12072  coprm  12098  prmrp  12099  isprm6  12101  prmdvdsexpb  12103  rpexp  12107  cncongrprm  12111  sqrt2irraplemnn  12133  phibndlem  12170  phiprmpw  12176  eulerthlemh  12185  eulerthlemth  12186  fermltl  12188  prmdivdiv  12191  modprm1div  12201  m1dvdsndvds  12202  coprimeprodsq  12211  pczpre  12251  pczcl  12252  pcexp  12263  pczdvds  12267  pczndvds  12269  pczndvds2  12271  pcdvdsb  12273  pcneg  12278  pcprmpw  12287  difsqpwdvds  12291  pcmptcl  12294  pcprod  12298  fldivp1  12300  infpnlem2  12312  1arithlem4  12318  ennnfonelemrn  12374  topnidg  12592  mgmlrid  12633  mndass  12660  mhmco  12705  grpass  12717  grpinvex  12718  dfgrp2  12732  grplid  12736  grprid  12737  grprcan  12740  tgss3  12872  clsval  12905  clsss3  12924  neiss2  12936  resttop  12964  resttopon2  12972  lmconst  13010  cnima  13014  cnntri  13018  cncnp  13024  cnrest  13029  cndis  13035  lmss  13040  lmff  13043  lmtopcnp  13044  txcnp  13065  upxp  13066  uptx  13068  cnmpt11  13077  hmeoima  13104  hmeoopn  13105  hmeocld  13106  hmeontr  13107  hmeoimaf1o  13108  mettri2  13156  met0  13158  metres2  13175  blpnf  13194  xblss2ps  13198  xblss2  13199  blbas  13227  blres  13228  xmetec  13231  mopnss  13244  xmstri2  13264  mstri2  13265  xmstri  13266  mstri  13267  xmstri3  13268  mstri3  13269  msrtri  13270  mopni3  13278  unimopn  13280  comet  13293  bdxmet  13295  climcncf  13365  dedekindeulemuub  13389  dedekindicclemuub  13398  dvfgg  13451  dvidlemap  13454  dvfre  13468  reeff1olem  13486  reeff1o  13488  sinperlem  13523  abssinper  13561  reexplog  13586  relogexp  13587  cxpexpnn  13611  cxprec  13625  abscxp  13629  lgsdir  13730  lgsprme0  13737  lgsdinn0  13743  bj-inex  13942  bj-nn0suc  13999  bj-nn0sucALT  14013  trilpolemeq1  14072  trilpolemlt1  14073  trirec0  14076  nconstwlpolemgt0  14095