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  7346  supisolem  7348  inflbti  7364  ordiso2  7375  djuex  7383  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  ctssdccl  7451  enumctlemm  7454  nnnninf  7466  finomni  7480  pm54.43  7536  acfun  7563  ccfunen  7630  cc2lem  7632  cc3  7634  addclpi  7694  addasspig  7697  mulasspig  7699  addnidpig  7703  nnppipi  7710  ltanqi  7769  ltmnqi  7770  ltexnqq  7775  archnqq  7784  prarloclemarch2  7786  enq0sym  7799  enq0tr  7801  nqnq0pi  7805  nqnq0  7808  mulcanenq0ec  7812  addclnq0  7818  nqpnq0nq  7820  distrnq0  7826  addassnq0lemcl  7828  addassnq0  7829  prubl  7853  prarloclemlt  7860  genpdf  7875  genipv  7876  genpelvl  7879  genpelvu  7880  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  genpassl  7891  genpassu  7892  genpassg  7893  addnqprl  7896  addnqpru  7897  addlocpr  7903  nqprm  7909  nqprl  7918  nqpru  7919  mulnqprl  7935  mulnqpru  7936  mullocprlem  7937  mullocpr  7938  addcomprg  7945  mulcomprg  7947  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  ltprordil  7956  1idprl  7957  1idpru  7958  ltpopr  7962  ltsopr  7963  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  prplnqu  7987  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  aptiprleml  8006  aptiprlemu  8007  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemloc  8042  caucvgprlemladdrl  8045  caucvgprprlemml  8061  caucvgprprlemloc  8070  00sr  8136  map2psrprg  8172  suplocsrlempr  8174  suplocsrlem  8175  adddir  8317  axsuploc  8398  eqle  8417  le2tri3i  8435  mul4  8459  muladd11  8460  cnegexlem3  8504  addsub12  8540  2addsub  8541  addsubeq4  8542  subadd4  8571  negcon1  8579  negdi2  8585  negsubdi2  8586  neg2sub  8587  renegcl  8588  muladd  8712  subdir  8714  gt0ne0  8756  ltnegcon1  8792  lenegcon1  8795  eqord1  8812  eqord2  8813  recexre  8908  ltmul1  8922  recexap  8983  div12ap  9026  rerecapb  9175  p1le  9181  ltmul2  9188  gt0div  9202  ge0div  9203  zlem1lt  9705  nnaddm1cl  9710  zdceq  9724  gtndiv  9745  prime  9749  msqznn  9750  btwnz  9769  uzss  9952  eluzadd  9960  nn0pzuz  9996  supinfneg  10004  infsupneg  10005  divfnzn  10030  qnegcl  10045  qreccl  10051  elpqb  10060  xaddass  10281  xleadd1a  10285  xlesubadd  10295  elico2  10349  iccss  10353  iccsupr  10378  elfz5  10430  fznn  10506  difelfznle  10552  fzoaddel  10615  elincfzoext  10621  qdceq  10689  qbtwnxr  10702  flqbi2  10739  adddivflid  10740  fldivnn0  10743  divfl0  10744  flqmulnn0  10747  fldivnn0le  10751  fldiv4p1lem1div2  10753  ceiqle  10763  flqdiv  10771  modqmulnn  10792  frecuzrdgtcl  10862  frecuzrdgsuc  10864  frecuzrdgdomlem  10867  frecuzrdgfunlem  10869  frecuzrdgsuctlem  10873  seqm1g  10924  seq3caopr2  10943  seqcaopr2g  10944  iseqf1olemkle  10947  seq3f1olemp  10965  seqf1oglem2  10970  seqf1og  10971  seq3id  10975  seq3z  10978  expap0  11019  mulexp  11028  mulexpzap  11029  expmul  11034  leexp1a  11044  expubnd  11046  zesq  11109  bernneq  11111  bernneq3  11113  modqexp  11117  facdiv  11190  facndiv  11191  faclbnd3  11195  faclbnd6  11196  bccmpl  11206  bcpasc  11218  bccl  11219  hashfibclem  11296  hashfibc  11297  seq3coll  11308  fundm2domnop  11315  wrdsymb1  11355  ccatfv0  11385  ccatrn  11391  ccat2s1cl  11415  lswccats1fst  11426  swrdspsleq  11453  pfxtrcfv  11479  pfxsuffeqwrdeq  11484  pfxlswccat  11499  wrdeqs1cat  11506  cats1un  11507  swrdccatin1  11511  pfxccatin12lem4  11512  swrdccatin2  11515  pfxccatin12  11519  swrdccat  11521  shftlem  11595  ovshftex  11598  shftval4  11607  shftf  11609  shftcan2  11614  crim  11637  mulreap  11643  remul2  11652  immul2  11659  cjexp  11672  caucvgre  11761  r19.2uz  11773  sqrtsq2  11823  absnid  11853  absexp  11860  nn0abscl  11866  abslt  11869  lenegsq  11876  cau3lem  11895  minmax  12011  xrmaxadd  12043  clim  12063  climshftlemg  12084  climcn1  12090  climcn1lem  12101  clim2ser  12119  clim2ser2  12120  iserex  12121  isermulc2  12122  climub  12126  climcaucn  12133  serf0  12134  summodclem3  12163  summodclem2a  12164  summodclem2  12165  summodc  12166  fsum3  12170  fsumf1o  12173  fisumss  12175  isumss2  12176  fsumcl2lem  12181  fsumadd  12189  fsumsplit  12190  isummulc2  12209  fsum2d  12218  fsummulc2  12231  telfsumo  12249  fsumparts  12253  hash2iun1dif1  12263  bcxmas  12272  isumshft  12273  isumsplit  12274  expcnvap0  12285  geolim  12294  geolim2  12295  cvgratnnlemmn  12308  cvgratnnlemseq  12309  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  clim2divap  12323  prodmodclem3  12358  prodmodclem2a  12359  fprodseq  12366  fprodf1o  12371  fprodmul  12374  fprodsplitdc  12379  efcllemp  12441  reefcl  12451  efcj  12456  efaddlem  12457  efexp  12465  reeftlcl  12472  eftlub  12473  efsep  12474  effsumlt  12475  eflegeo  12484  retanclap  12505  demoivre  12556  demoivreALT  12557  eirraplem  12560  dvdsval3  12574  p1modz1  12577  iddvdsexp  12598  alzdvds  12637  addmodlteqALT  12642  nnehalf  12687  nno  12689  ndvdsadd  12714  bitsp1e  12735  bitsp1o  12736  bitsinv1  12745  divgcdnnr  12769  neggcd  12776  gcdabs  12781  bezoutlemmain  12791  bezoutlemaz  12796  bezoutlembz  12797  gcdmultiplez  12814  gcdzeq  12815  dvdssq  12824  nninfctlemfo  12833  algrf  12839  algcvg  12842  algcvga  12845  algfx  12846  eucalgf  12849  eucalgcvga  12852  neglcm  12869  lcmabs  12870  lcmdvds  12873  lcmgcdeq  12877  qredeq  12890  isprm3  12912  coprm  12939  prmrp  12940  isprm6  12942  prmdvdsexpb  12944  rpexp  12948  cncongrprm  12952  sqrt2irraplemnn  12975  phibndlem  13014  phiprmpw  13020  eulerthlemh  13029  eulerthlemth  13030  fermltl  13032  prmdivdiv  13035  modprm1div  13046  m1dvdsndvds  13047  coprimeprodsq  13056  pczpre  13096  pczcl  13097  pcexp  13108  pczdvds  13113  pczndvds  13115  pczndvds2  13117  pcdvdsb  13119  pcneg  13124  pcprmpw  13133  difsqpwdvds  13137  pcmptcl  13141  pcprod  13145  fldivp1  13147  infpnlem2  13159  1arithlem4  13165  prmlem0  13240  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemfrcn0  13322  ennnfonelemrn  13359  topnidg  13655  imasaddfnlemg  13684  imasaddflemg  13686  qusin  13696  mgmlrid  13748  mndass  13786  mhmco  13846  gzsumwcl  13851  gzsumwmhm  13852  grpass  13863  grpinvex  13864  dfgrp2  13881  grplid  13885  grprid  13886  grprcan  13891  grpinvssd  13931  grpinvval2  13937  mhmid  13967  mhmmnd  13968  ghmgrp  13970  mulgnn  13978  mulgnnp1  13982  mulgnegnn  13984  mulgnnsubcl  13986  mulgz  14002  issubg2m  14041  issubg4m  14045  subgintm  14050  nmzbi  14061  eqger  14076  eqgid  14078  eqgen  14079  qusgrp  14084  qusadd  14086  qusinv  14088  qussub  14089  ghminv  14102  ghmsub  14103  ghmrn  14109  resghm2b  14114  ghmf1  14125  conjsubg  14129  conjsubgen  14130  qusghm  14134  cmncom  14154  ablsubadd  14165  ablsubsub23  14178  ghmcmn  14180  gzsumreidx  14190  gsumsubmfi  14217  prdsidlem  14242  prdsinvlem  14245  pwselbasb  14255  pwsplusgval  14257  pwsmulrval  14258  pwsinvg  14264  mgpress  14279  srg1expzeq1  14348  ringinvnz1ne0  14403  ringinvnzdiv  14404  dvdsrd  14450  dvdsunit  14468  unitinvcl  14479  unitinvinv  14480  unitlinv  14482  unitrinv  14483  rhmunitinv  14534  subrngintm  14569  subrg1  14588  subrguss  14593  subrginv  14594  subrgunit  14596  subrgugrp  14597  subrgintm  14600  resrhm  14605  resrhm2b  14606  lmodass  14688  lmodlcan  14689  lmod0vlid  14704  lmod0vrid  14705  lmod0vid  14706  lmodvs0  14708  lcomf  14713  lmodvnegcl  14714  lmodvnegid  14715  lmodvsubadd  14724  lmodsubid  14733  lss1d  14769  lspval  14776  ellspsn6  14794  lspsnneg  14806  sralmod  14836  dflidl2rng  14867  lidlacl  14870  dflidl2  14874  df2idl2  14895  qusmul2  14915  quscrng  14919  cnfldmulg  14962  znf1o  15035  znidom  15041  aspval  15064  asclghm  15074  issubassa2  15084  psraddcl  15120  psr0lid  15122  tgss3  15228  clsval  15261  clsss3  15280  neiss2  15292  resttop  15320  resttopon2  15328  lmconst  15366  cnima  15370  cnntri  15374  cncnp  15380  cnrest  15385  cndis  15391  lmss  15396  lmff  15399  lmtopcnp  15400  txcnp  15421  upxp  15422  uptx  15424  cnmpt11  15433  hmeoima  15460  hmeoopn  15461  hmeocld  15462  hmeontr  15463  hmeoimaf1o  15464  mettri2  15512  met0  15514  metres2  15531  blpnf  15550  xblss2ps  15554  xblss2  15555  blbas  15583  blres  15584  xmetec  15587  mopnss  15600  xmstri2  15620  mstri2  15621  xmstri  15622  mstri  15623  xmstri3  15624  mstri3  15625  msrtri  15626  mopni3  15634  unimopn  15636  comet  15649  bdxmet  15651  climcncf  15734  dedekindeulemuub  15767  dedekindicclemuub  15776  ivthdichlem  15801  dvfgg  15838  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvfre  15860  dvmptfsum  15875  plyadd  15901  plymul  15902  reeff1olem  15921  reeff1o  15923  sinperlem  15959  abssinper  15997  reexplog  16023  relogexp  16024  cxpexpnn  16051  cxprec  16065  rpcxpmul2  16068  abscxp  16070  wilthlem1  16151  ppival2g  16162  sgmval2  16165  sgmnncl  16169  0sgmppw  16188  perfectlem1  16197  bposlem3  16211  bposlem5  16213  lgsdir  16252  lgsprme0  16259  lgsdinn0  16265  gausslemma2dlem3  16280  gausslemma2dlem5a  16282  2lgslem1a2  16304  2lgslem1a  16305  2lgslem3  16318  2lgs  16321  umgredgprv  16454  umgrislfupgrdom  16470  uspgredgiedg  16517  uspgriedgedg  16518  usgrislfuspgrdom  16529  usgredg2en  16534  usgredgprv  16535  usgrpredgv  16537  usgredg  16539  usgrnloopv  16540  usgredgne  16543  usgredg3  16553  usgredgedg  16566  usgredgdomord  16569  usgr1vr  16587  subgruhgrfun  16607  subupgr  16612  subumgr  16613  subusgr  16614  umgrwlknloop  16707  wlkres  16718  clwwlkccatlem  16739  clwwlkccat  16740  depindlem1  16845  depindlem2  16846  depindlem3  16847  bj-inex  17031  bj-nn0suc  17088  bj-nn0sucALT  17102  trilpolemeq1  17187  trilpolemlt1  17188  trirec0  17191  nconstwlpolemgt0  17212