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  940  3adantl1  1155  3adantl2  1156  3adantl3  1157  syl3anl1  1297  syl3anl3  1299  syl3anl  1300  stoic3  1442  eupick  2121  csbiebt  3120  csbnestgf  3133  reuss2  3439  mpteq12  4112  otexg  4259  opelopabt  4292  sonr  4348  sotr  4349  issod  4350  so2nr  4352  so3nr  4353  ordelss  4410  onelon  4415  elrnmpt1s  4912  iota2  5244  funeu  5279  imadif  5334  fnbr  5356  feu  5436  f1ss  5465  f1ssres  5468  f1resf1  5469  dffo2  5480  foco  5487  foun  5519  fun11iun  5521  ffoss  5532  funbrfv  5595  fvco3  5628  fvopab6  5654  funfvbrb  5671  elpreima  5677  ffvelcdm  5691  ffvelcdmda  5693  dffo4  5706  fmptco  5724  fsn2  5732  fvconst2g  5772  fex  5787  funfvima  5790  f1elima  5816  f1ocnvfv1  5820  f1ocnvfv2  5821  cocan2  5831  foeqcnvco  5833  isocnv  5854  isores2  5856  isoini  5861  isoselem  5863  f1oiso  5869  f1ofveu  5906  eloprabga  6005  suppssof1  6148  ofco  6149  offveqb  6150  ofc1g  6151  ofc2g  6152  fnexALT  6163  f1dmex  6168  ot1stg  6205  ot2ndg  6206  ot3rdgg  6207  eqopi  6225  2ndrn  6236  fo2ndf  6280  smores3  6346  smores2  6347  smoel  6353  smoiso  6355  tfrlem1  6361  tfrlemisucaccv  6378  tfrlemibxssdm  6380  tfrlemiubacc  6383  tfr1onlemsucaccv  6394  tfr1onlembfn  6397  tfr1onlemubacc  6399  tfr1onlemaccex  6401  tfr1onlemres  6402  tfrcllemsucaccv  6407  tfrcllembfn  6410  tfrcllemubacc  6412  tfrcllemaccex  6414  tfrcllemres  6415  tfrcl  6417  frecrdg  6461  omv2  6518  nnasuc  6529  nnmsuc  6530  nnacom  6537  nnaass  6538  nnmass  6540  nntri1  6549  nndifsnid  6560  nnmordi  6569  swoer  6615  erth  6633  riinerm  6662  qliftlem  6667  ecovass  6698  ecoviass  6699  elmapssres  6727  fvixp  6757  f1domg  6812  endomtr  6844  xpsnen2g  6883  enen1  6896  enen2  6897  domen1  6898  domen2  6899  mapen  6902  mapxpen  6904  ssenen  6907  phplem1  6908  fidifsnid  6927  findcard  6944  findcard2  6945  findcard2s  6946  fieq0  7035  isotilem  7065  supisolem  7067  inflbti  7083  ordiso2  7094  djuex  7102  updjudhcoinlf  7139  updjudhcoinrg  7140  updjud  7141  ctssdccl  7170  enumctlemm  7173  nnnninf  7185  finomni  7199  pm54.43  7250  acfun  7267  ccfunen  7324  cc2lem  7326  cc3  7328  addclpi  7387  addasspig  7390  mulasspig  7392  addnidpig  7396  nnppipi  7403  ltanqi  7462  ltmnqi  7463  ltexnqq  7468  archnqq  7477  prarloclemarch2  7479  enq0sym  7492  enq0tr  7494  nqnq0pi  7498  nqnq0  7501  mulcanenq0ec  7505  addclnq0  7511  nqpnq0nq  7513  distrnq0  7519  addassnq0lemcl  7521  addassnq0  7522  prubl  7546  prarloclemlt  7553  genpdf  7568  genipv  7569  genpelvl  7572  genpelvu  7573  genpml  7577  genpmu  7578  genprndl  7581  genprndu  7582  genpassl  7584  genpassu  7585  genpassg  7586  addnqprl  7589  addnqpru  7590  addlocpr  7596  nqprm  7602  nqprl  7611  nqpru  7612  mulnqprl  7628  mulnqpru  7629  mullocprlem  7630  mullocpr  7631  addcomprg  7638  mulcomprg  7640  distrlem1prl  7642  distrlem1pru  7643  distrlem4prl  7644  distrlem4pru  7645  ltprordil  7649  1idprl  7650  1idpru  7651  ltpopr  7655  ltsopr  7656  ltaddpr  7657  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  prplnqu  7680  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1l  7695  recexprlemss1u  7696  aptiprleml  7699  aptiprlemu  7700  cauappcvgprlemloc  7712  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemloc  7735  caucvgprlemladdrl  7738  caucvgprprlemml  7754  caucvgprprlemloc  7763  00sr  7829  map2psrprg  7865  suplocsrlempr  7867  suplocsrlem  7868  adddir  8010  axsuploc  8092  eqle  8111  le2tri3i  8128  mul4  8151  muladd11  8152  cnegexlem3  8196  addsub12  8232  2addsub  8233  addsubeq4  8234  subadd4  8263  negcon1  8271  negdi2  8277  negsubdi2  8278  neg2sub  8279  renegcl  8280  muladd  8403  subdir  8405  gt0ne0  8446  ltnegcon1  8482  lenegcon1  8485  eqord1  8502  eqord2  8503  recexre  8597  ltmul1  8611  recexap  8672  div12ap  8713  rerecapb  8862  p1le  8868  ltmul2  8875  gt0div  8889  ge0div  8890  zlem1lt  9373  nnaddm1cl  9378  zdceq  9392  gtndiv  9412  prime  9416  msqznn  9417  btwnz  9436  uzss  9613  eluzadd  9621  nn0pzuz  9652  supinfneg  9660  infsupneg  9661  divfnzn  9686  qnegcl  9701  qreccl  9707  elpqb  9715  xaddass  9935  xleadd1a  9939  xlesubadd  9949  elico2  10003  iccss  10007  iccsupr  10032  elfz5  10083  fznn  10155  difelfznle  10201  fzoaddel  10259  qdceq  10314  qbtwnxr  10326  flqbi2  10360  adddivflid  10361  fldivnn0  10364  divfl0  10365  flqmulnn0  10368  fldivnn0le  10372  fldiv4p1lem1div2  10374  ceiqle  10384  flqdiv  10392  modqmulnn  10413  frecuzrdgtcl  10483  frecuzrdgsuc  10485  frecuzrdgdomlem  10488  frecuzrdgfunlem  10490  frecuzrdgsuctlem  10494  seqm1g  10545  seq3caopr2  10564  seqcaopr2g  10565  iseqf1olemkle  10568  seq3f1olemp  10586  seqf1oglem2  10591  seqf1og  10592  seq3id  10596  seq3z  10599  expap0  10640  mulexp  10649  mulexpzap  10650  expmul  10655  leexp1a  10665  expubnd  10667  zesq  10729  bernneq  10731  bernneq3  10733  modqexp  10737  facdiv  10809  facndiv  10810  faclbnd3  10814  faclbnd6  10815  bccmpl  10825  bcpasc  10837  bccl  10838  seq3coll  10913  wrdsymb1  10950  shftlem  10960  ovshftex  10963  shftval4  10972  shftf  10974  shftcan2  10979  crim  11002  mulreap  11008  remul2  11017  immul2  11024  cjexp  11037  caucvgre  11125  r19.2uz  11137  sqrtsq2  11187  absnid  11217  absexp  11223  nn0abscl  11229  abslt  11232  lenegsq  11239  cau3lem  11258  minmax  11373  xrmaxadd  11404  clim  11424  climshftlemg  11445  climcn1  11451  climcn1lem  11462  clim2ser  11480  clim2ser2  11481  iserex  11482  isermulc2  11483  climub  11487  climcaucn  11494  serf0  11495  summodclem3  11523  summodclem2a  11524  summodclem2  11525  summodc  11526  fsum3  11530  fsumf1o  11533  fisumss  11535  isumss2  11536  fsumcl2lem  11541  fsumadd  11549  fsumsplit  11550  isummulc2  11569  fsum2d  11578  fsummulc2  11591  telfsumo  11609  fsumparts  11613  hash2iun1dif1  11623  bcxmas  11632  isumshft  11633  isumsplit  11634  expcnvap0  11645  geolim  11654  geolim2  11655  cvgratnnlemmn  11668  cvgratnnlemseq  11669  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  clim2divap  11683  prodmodclem3  11718  prodmodclem2a  11719  fprodseq  11726  fprodf1o  11731  fprodmul  11734  fprodsplitdc  11739  efcllemp  11801  reefcl  11811  efcj  11816  efaddlem  11817  efexp  11825  reeftlcl  11832  eftlub  11833  efsep  11834  effsumlt  11835  eflegeo  11844  retanclap  11865  demoivre  11916  demoivreALT  11917  eirraplem  11920  dvdsval3  11934  p1modz1  11937  iddvdsexp  11958  alzdvds  11996  addmodlteqALT  12001  nnehalf  12045  nno  12047  ndvdsadd  12072  divgcdnnr  12113  neggcd  12120  gcdabs  12125  bezoutlemmain  12135  bezoutlemaz  12140  bezoutlembz  12141  gcdmultiplez  12158  gcdzeq  12159  dvdssq  12168  nninfctlemfo  12177  algrf  12183  algcvg  12186  algcvga  12189  algfx  12190  eucalgf  12193  eucalgcvga  12196  neglcm  12213  lcmabs  12214  lcmdvds  12217  lcmgcdeq  12221  qredeq  12234  isprm3  12256  coprm  12282  prmrp  12283  isprm6  12285  prmdvdsexpb  12287  rpexp  12291  cncongrprm  12295  sqrt2irraplemnn  12317  phibndlem  12354  phiprmpw  12360  eulerthlemh  12369  eulerthlemth  12370  fermltl  12372  prmdivdiv  12375  modprm1div  12385  m1dvdsndvds  12386  coprimeprodsq  12395  pczpre  12435  pczcl  12436  pcexp  12447  pczdvds  12452  pczndvds  12454  pczndvds2  12456  pcdvdsb  12458  pcneg  12463  pcprmpw  12472  difsqpwdvds  12476  pcmptcl  12480  pcprod  12484  fldivp1  12486  infpnlem2  12498  1arithlem4  12504  ennnfonelemrn  12576  topnidg  12863  imasaddfnlemg  12897  imasaddflemg  12899  qusin  12909  mgmlrid  12962  mndass  13005  mhmco  13062  gsumsubm  13066  gsumwcl  13069  gsumwmhm  13070  grpass  13081  grpinvex  13082  dfgrp2  13099  grplid  13103  grprid  13104  grprcan  13109  grpinvssd  13149  grpinvval2  13155  mhmid  13185  mhmmnd  13186  ghmgrp  13188  mulgnn  13196  mulgnnp1  13200  mulgnegnn  13202  mulgnnsubcl  13204  mulgz  13220  issubg2m  13259  issubg4m  13263  subgintm  13268  nmzbi  13279  eqger  13294  eqgid  13296  eqgen  13297  qusgrp  13302  qusadd  13304  qusinv  13306  qussub  13307  ghminv  13320  ghmsub  13321  ghmrn  13327  resghm2b  13332  ghmf1  13343  conjsubg  13347  conjsubgen  13348  qusghm  13352  cmncom  13372  ablsubadd  13382  ablsubsub23  13395  ghmcmn  13397  gsumfzreidx  13407  mgpress  13427  srg1expzeq1  13491  ringinvnz1ne0  13545  ringinvnzdiv  13546  dvdsrd  13590  dvdsunit  13608  unitinvcl  13619  unitinvinv  13620  unitlinv  13622  unitrinv  13623  rhmunitinv  13674  subrngintm  13708  subrg1  13727  subrguss  13732  subrginv  13733  subrgunit  13735  subrgugrp  13736  subrgintm  13739  resrhm  13744  resrhm2b  13745  lmodass  13799  lmodlcan  13800  lmod0vlid  13814  lmod0vrid  13815  lmod0vid  13816  lmodvs0  13818  lcomf  13823  lmodvnegcl  13824  lmodvnegid  13825  lmodvsubadd  13834  lmodsubid  13843  lss1d  13879  lspval  13886  lspsnel6  13904  lspsnneg  13916  sralmod  13946  dflidl2rng  13977  lidlacl  13980  dflidl2  13984  df2idl2  14005  qusmul2  14025  quscrng  14029  cnfldmulg  14064  znf1o  14139  znidom  14145  psraddcl  14164  tgss3  14246  clsval  14279  clsss3  14298  neiss2  14310  resttop  14338  resttopon2  14346  lmconst  14384  cnima  14388  cnntri  14392  cncnp  14398  cnrest  14403  cndis  14409  lmss  14414  lmff  14417  lmtopcnp  14418  txcnp  14439  upxp  14440  uptx  14442  cnmpt11  14451  hmeoima  14478  hmeoopn  14479  hmeocld  14480  hmeontr  14481  hmeoimaf1o  14482  mettri2  14530  met0  14532  metres2  14549  blpnf  14568  xblss2ps  14572  xblss2  14573  blbas  14601  blres  14602  xmetec  14605  mopnss  14618  xmstri2  14638  mstri2  14639  xmstri  14640  mstri  14641  xmstri3  14642  mstri3  14643  msrtri  14644  mopni3  14652  unimopn  14654  comet  14667  bdxmet  14669  climcncf  14739  dedekindeulemuub  14771  dedekindicclemuub  14780  ivthdichlem  14805  dvfgg  14842  dvidlemap  14845  dvfre  14859  plyadd  14897  plymul  14898  reeff1olem  14906  reeff1o  14908  sinperlem  14943  abssinper  14981  reexplog  15006  relogexp  15007  cxpexpnn  15031  cxprec  15045  abscxp  15049  wilthlem1  15112  lgsdir  15151  lgsprme0  15158  lgsdinn0  15164  gausslemma2dlem3  15179  gausslemma2dlem5a  15181  bj-inex  15399  bj-nn0suc  15456  bj-nn0sucALT  15470  trilpolemeq1  15530  trilpolemlt1  15531  trirec0  15534  nconstwlpolemgt0  15554