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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylanb  284  sylanbr  285  syl2an  289  sylanl1  406  sylanl2  407  mpanl1  438  mpanl2  439  syldanl  453  adantll  480  adantlr  481  ancom1s  575  pm4.55dc  951  dfifp2dc  994  3adantl1  1184  3adantl2  1185  3adantl3  1186  syl3anl1  1326  syl3anl3  1328  syl3anl  1329  stoic3  1480  eupick  2166  csbiebt  3187  csbnestgf  3200  reuss2  3513  mpteq12  4214  otexg  4370  opelopabt  4404  sonr  4462  sotr  4463  issod  4464  so2nr  4466  so3nr  4467  ordelss  4524  onelon  4529  elrnmpt1s  5032  iota2  5367  funeu  5402  imadif  5461  fnbr  5485  feu  5574  f1ss  5604  f1ssres  5607  f1resf1  5608  dffo2  5619  foco  5626  foun  5658  fun11iun  5660  ffoss  5672  funbrfv  5739  fvco3  5776  fvopab6  5805  funfvbrb  5822  elpreima  5828  ffvelcdm  5841  ffvelcdmda  5843  dffo4  5856  fmptco  5874  fsn2  5882  fncofn  5893  fvconst2g  5929  fex  5947  funfvima  5950  f1elima  5979  f1ocnvfv1  5983  f1ocnvfv2  5984  cocan2  5994  foeqcnvco  5996  isocnv  6017  isores2  6019  isoini  6024  isoselem  6026  f1oiso  6032  f1ofveu  6073  eloprabga  6175  suppssof1  6320  ofco  6321  offveqb  6322  ofc1g  6324  ofc2g  6325  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  fnexALT  6340  f1dmex  6345  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  eqopi  6406  2ndrn  6417  fo2ndf  6463  suppval1  6479  ressuppss  6494  suppssrst  6501  suppssrgst  6502  smores3  6564  smores2  6565  smoel  6571  smoiso  6573  tfrlem1  6579  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemiubacc  6601  tfr1onlemsucaccv  6612  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  frecrdg  6679  omv2  6738  nnasuc  6749  nnmsuc  6750  nnacom  6757  nnaass  6758  nnmass  6760  nntri1  6769  nndifsnid  6780  nnmordi  6789  swoer  6835  erth  6853  riinerm  6882  qliftlem  6887  ecovass  6918  ecoviass  6919  elmapssres  6954  fvixp  6985  f1domg  7044  domssr  7064  endomtr  7077  xpsnen2g  7127  enen1  7140  enen2  7141  domen1  7142  domen2  7143  mapen  7146  mapxpen  7148  ssenen  7152  phplem1  7153  fidifsnid  7173  findcard  7192  findcard2  7193  findcard2s  7194  fidcen  7203  fieq0  7310  isotilem  7347  supisolem  7349  inflbti  7365  ordiso2  7376  djuex  7384  updjudhcoinlf  7421  updjudhcoinrg  7422  updjud  7423  ctssdccl  7452  enumctlemm  7455  nnnninf  7467  finomni  7481  pm54.43  7537  acfun  7564  ccfunen  7631  cc2lem  7633  cc3  7635  addclpi  7695  addasspig  7698  mulasspig  7700  addnidpig  7704  nnppipi  7711  ltanqi  7770  ltmnqi  7771  ltexnqq  7776  archnqq  7785  prarloclemarch2  7787  enq0sym  7800  enq0tr  7802  nqnq0pi  7806  nqnq0  7809  mulcanenq0ec  7813  addclnq0  7819  nqpnq0nq  7821  distrnq0  7827  addassnq0lemcl  7829  addassnq0  7830  prubl  7854  prarloclemlt  7861  genpdf  7876  genipv  7877  genpelvl  7880  genpelvu  7881  genpml  7885  genpmu  7886  genprndl  7889  genprndu  7890  genpassl  7892  genpassu  7893  genpassg  7894  addnqprl  7897  addnqpru  7898  addlocpr  7904  nqprm  7910  nqprl  7919  nqpru  7920  mulnqprl  7936  mulnqpru  7937  mullocprlem  7938  mullocpr  7939  addcomprg  7946  mulcomprg  7948  distrlem1prl  7950  distrlem1pru  7951  distrlem4prl  7952  distrlem4pru  7953  ltprordil  7957  1idprl  7958  1idpru  7959  ltpopr  7963  ltsopr  7964  ltaddpr  7965  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  prplnqu  7988  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  aptiprleml  8007  aptiprlemu  8008  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemloc  8043  caucvgprlemladdrl  8046  caucvgprprlemml  8062  caucvgprprlemloc  8071  00sr  8137  map2psrprg  8173  suplocsrlempr  8175  suplocsrlem  8176  adddir  8318  axsuploc  8399  eqle  8418  le2tri3i  8436  mul4  8460  muladd11  8461  cnegexlem3  8505  addsub12  8541  2addsub  8542  addsubeq4  8543  subadd4  8572  negcon1  8580  negdi2  8586  negsubdi2  8587  neg2sub  8588  renegcl  8589  muladd  8713  subdir  8715  gt0ne0  8757  ltnegcon1  8793  lenegcon1  8796  eqord1  8813  eqord2  8814  recexre  8909  ltmul1  8923  recexap  8984  div12ap  9027  rerecapb  9176  p1le  9182  ltmul2  9189  gt0div  9203  ge0div  9204  zlem1lt  9706  nnaddm1cl  9711  zdceq  9725  gtndiv  9746  prime  9750  msqznn  9751  btwnz  9770  uzss  9953  eluzadd  9961  nn0pzuz  9997  supinfneg  10005  infsupneg  10006  divfnzn  10031  qnegcl  10046  qreccl  10052  elpqb  10061  xaddass  10282  xleadd1a  10286  xlesubadd  10296  elico2  10350  iccss  10354  iccsupr  10379  elfz5  10431  fznn  10507  difelfznle  10553  fzoaddel  10616  elincfzoext  10622  qdceq  10690  qbtwnxr  10703  flqbi2  10741  adddivflid  10742  fldivnn0  10745  divfl0  10746  flqmulnn0  10749  fldivnn0le  10753  fldiv4p1lem1div2  10755  ceiqle  10765  flqdiv  10773  modqmulnn  10794  frecuzrdgtcl  10864  frecuzrdgsuc  10866  frecuzrdgdomlem  10869  frecuzrdgfunlem  10871  frecuzrdgsuctlem  10875  seqm1g  10926  seq3caopr2  10945  seqcaopr2g  10946  iseqf1olemkle  10949  seq3f1olemp  10967  seqf1oglem2  10972  seqf1og  10973  seq3id  10977  seq3z  10980  expap0  11021  mulexp  11030  mulexpzap  11031  expmul  11036  leexp1a  11046  expubnd  11048  zesq  11111  bernneq  11113  bernneq3  11115  modqexp  11119  facdiv  11192  facndiv  11193  faclbnd3  11197  faclbnd6  11198  bccmpl  11208  bcpasc  11220  bccl  11221  hashfibclem  11298  hashfibc  11299  seq3coll  11310  fundm2domnop  11317  wrdsymb1  11357  ccatfv0  11387  ccatrn  11393  ccat2s1cl  11417  lswccats1fst  11428  swrdspsleq  11455  pfxtrcfv  11481  pfxsuffeqwrdeq  11486  pfxlswccat  11501  wrdeqs1cat  11508  cats1un  11509  swrdccatin1  11513  pfxccatin12lem4  11514  swrdccatin2  11517  pfxccatin12  11521  swrdccat  11523  shftlem  11597  ovshftex  11600  shftval4  11609  shftf  11611  shftcan2  11616  crim  11639  mulreap  11645  remul2  11654  immul2  11661  cjexp  11674  caucvgre  11763  r19.2uz  11775  sqrtsq2  11825  absnid  11855  absexp  11862  nn0abscl  11868  abslt  11871  lenegsq  11878  cau3lem  11897  minmax  12014  xrmaxadd  12046  clim  12066  climshftlemg  12087  climcn1  12093  climcn1lem  12104  clim2ser  12122  clim2ser2  12123  iserex  12124  isermulc2  12125  climub  12129  climcaucn  12136  serf0  12137  summodclem3  12166  summodclem2a  12167  summodclem2  12168  summodc  12169  fsum3  12173  fsumf1o  12176  fisumss  12178  isumss2  12179  fsumcl2lem  12184  fsumadd  12192  fsumsplit  12193  isummulc2  12212  fsum2d  12221  fsummulc2  12234  telfsumo  12252  fsumparts  12256  hash2iun1dif1  12266  bcxmas  12275  isumshft  12276  isumsplit  12277  expcnvap0  12288  geolim  12297  geolim2  12298  cvgratnnlemmn  12311  cvgratnnlemseq  12312  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  clim2divap  12326  prodmodclem3  12361  prodmodclem2a  12362  fprodseq  12369  fprodf1o  12374  fprodmul  12377  fprodsplitdc  12382  efcllemp  12444  reefcl  12454  efcj  12459  efaddlem  12460  efexp  12468  reeftlcl  12475  eftlub  12476  efsep  12477  effsumlt  12478  eflegeo  12487  retanclap  12508  demoivre  12559  demoivreALT  12560  eirraplem  12563  dvdsval3  12577  p1modz1  12580  iddvdsexp  12601  alzdvds  12640  addmodlteqALT  12645  nnehalf  12690  nno  12692  ndvdsadd  12717  bitsp1e  12738  bitsp1o  12739  bitsinv1  12748  divgcdnnr  12772  neggcd  12779  gcdabs  12784  bezoutlemmain  12794  bezoutlemaz  12799  bezoutlembz  12800  gcdmultiplez  12817  gcdzeq  12818  dvdssq  12827  nninfctlemfo  12836  algrf  12842  algcvg  12845  algcvga  12848  algfx  12849  eucalgf  12852  eucalgcvga  12855  neglcm  12872  lcmabs  12873  lcmdvds  12876  lcmgcdeq  12880  qredeq  12893  isprm3  12915  coprm  12942  prmrp  12943  isprm6  12945  prmdvdsexpb  12947  rpexp  12951  cncongrprm  12955  sqrt2irraplemnn  12978  phibndlem  13017  phiprmpw  13023  eulerthlemh  13032  eulerthlemth  13033  fermltl  13035  prmdivdiv  13038  modprm1div  13049  m1dvdsndvds  13050  coprimeprodsq  13059  pczpre  13099  pczcl  13100  pcexp  13111  pczdvds  13116  pczndvds  13118  pczndvds2  13120  pcdvdsb  13122  pcneg  13127  pcprmpw  13136  difsqpwdvds  13140  pcmptcl  13144  pcprod  13148  fldivp1  13150  infpnlem2  13162  1arithlem4  13168  prmlem0  13243  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemfrcn0  13325  ennnfonelemrn  13362  topnidg  13659  imasaddfnlemg  13688  imasaddflemg  13690  qusin  13700  mgmlrid  13752  mndass  13790  mhmco  13850  gzsumwcl  13855  gzsumwmhm  13856  grpass  13867  grpinvex  13868  dfgrp2  13885  grplid  13889  grprid  13890  grprcan  13895  grpinvssd  13935  grpinvval2  13941  mhmid  13971  mhmmnd  13972  ghmgrp  13974  mulgnn  13982  mulgnnp1  13986  mulgnegnn  13988  mulgnnsubcl  13990  mulgz  14006  issubg2m  14045  issubg4m  14049  subgintm  14054  nmzbi  14065  eqger  14080  eqgid  14082  eqgen  14083  qusgrp  14088  qusadd  14090  qusinv  14092  qussub  14093  ghminv  14106  ghmsub  14107  ghmrn  14113  resghm2b  14118  ghmf1  14129  conjsubg  14133  conjsubgen  14134  qusghm  14138  cntzi  14156  cntzsgrpcl  14161  cntzsubm  14164  cntzsubg  14165  cmncom  14189  ablsubadd  14200  ablsubsub23  14213  ghmcmn  14215  gzsumreidx  14225  gsumsubmfi  14252  prdsidlem  14277  prdsinvlem  14280  pwselbasb  14290  pwsplusgval  14292  pwsmulrval  14293  pwsinvg  14299  mgpress  14314  srg1expzeq1  14383  ringinvnz1ne0  14438  ringinvnzdiv  14439  dvdsrd  14485  dvdsunit  14503  unitinvcl  14514  unitinvinv  14515  unitlinv  14517  unitrinv  14518  rhmunitinv  14569  subrngintm  14604  subrg1  14623  subrguss  14628  subrginv  14629  subrgunit  14631  subrgugrp  14632  subrgintm  14635  resrhm  14640  resrhm2b  14641  lmodass  14723  lmodlcan  14724  lmod0vlid  14739  lmod0vrid  14740  lmod0vid  14741  lmodvs0  14743  lcomf  14748  lmodvnegcl  14749  lmodvnegid  14750  lmodvsubadd  14759  lmodsubid  14768  lss1d  14804  lspval  14811  ellspsn6  14829  lspsnneg  14841  sralmod  14871  dflidl2rng  14902  lidlacl  14905  dflidl2  14909  df2idl2  14930  qusmul2  14950  quscrng  14954  cnfldmulg  14997  znf1o  15070  znidom  15076  aspval  15099  asclghm  15109  issubassa2  15119  psraddcl  15156  psrmulvalfi  15160  psr0lid  15164  tgss3  15270  clsval  15303  clsss3  15322  neiss2  15334  resttop  15362  resttopon2  15370  lmconst  15408  cnima  15412  cnntri  15416  cncnp  15422  cnrest  15427  cndis  15433  lmss  15438  lmff  15441  lmtopcnp  15442  txcnp  15463  upxp  15464  uptx  15466  cnmpt11  15475  hmeoima  15502  hmeoopn  15503  hmeocld  15504  hmeontr  15505  hmeoimaf1o  15506  mettri2  15554  met0  15556  metres2  15573  blpnf  15592  xblss2ps  15596  xblss2  15597  blbas  15625  blres  15626  xmetec  15629  mopnss  15642  xmstri2  15662  mstri2  15663  xmstri  15664  mstri  15665  xmstri3  15666  mstri3  15667  msrtri  15668  mopni3  15676  unimopn  15678  comet  15691  bdxmet  15693  climcncf  15776  dedekindeulemuub  15809  dedekindicclemuub  15818  ivthdichlem  15843  dvfgg  15880  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvfre  15902  dvmptfsum  15917  plyadd  15943  plymul  15944  reeff1olem  15963  reeff1o  15965  sinperlem  16001  abssinper  16039  reexplog  16065  relogexp  16066  cxpexpnn  16093  cxprec  16107  rpcxpmul2  16110  abscxp  16112  wilthlem1  16193  ppival2g  16211  sgmval2  16214  sgmnncl  16218  0sgmppw  16248  chtublem  16256  perfectlem1  16260  bposlem3  16274  bposlem5  16276  bposlem6  16277  lgsdir  16320  lgsprme0  16327  lgsdinn0  16333  gausslemma2dlem3  16348  gausslemma2dlem5a  16350  2lgslem1a2  16372  2lgslem1a  16373  2lgslem3  16386  2lgs  16389  umgredgprv  16522  umgrislfupgrdom  16538  uspgredgiedg  16585  uspgriedgedg  16586  usgrislfuspgrdom  16597  usgredg2en  16602  usgredgprv  16603  usgrpredgv  16605  usgredg  16607  usgrnloopv  16608  usgredgne  16611  usgredg3  16621  usgredgedg  16634  usgredgdomord  16637  usgr1vr  16655  subgruhgrfun  16675  subupgr  16680  subumgr  16681  subusgr  16682  umgrwlknloop  16775  wlkres  16786  clwwlkccatlem  16807  clwwlkccat  16808  depindlem1  16913  depindlem2  16914  depindlem3  16915  bj-inex  17099  bj-nn0suc  17156  bj-nn0sucALT  17170  trilpolemeq1  17256  trilpolemlt1  17257  trirec0  17260  nconstwlpolemgt0  17281