Theorem sylan2 500

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylan.1	|- ((ph /\ ps) -> ch)
sylan2.2	|- (th -> ps)

Assertion

Ref	Expression
sylan2	|- ((ph /\ th) -> ch)

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 402	. . 3 |- (ph -> (ps -> ch))
3		sylan2.2	. . 3 |- (th -> ps)
4	2, 3	syl5 20	. 2 |- (ph -> (th -> ch))
5	4	imp 377	1 |- ((ph /\ th) -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  sylan2b 501  sylan2br 502  syl2an 503  sylanr1 511  sylanr2 512  ax11indalem 1759  ax11inda2ALT 1760  elabgt 2400  elabgtOLD 2401  sbciegft 2482  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  hbcsb1gd 2570  hbcsbgd 2571  csbnestg 2581  sbcnestg 2583  sspr 3144  ssiunOLD 3294  trssord 3675  ordelssne 3685  onsssuc 3757  onint 3876  onint0 3877  onnmin 3884  onsucmin 3901  ordsucun 3905  nlimsucgOLD 3924  ordunisuc2 3926  tfindsg 3944  tfindsg2 3945  peano5 3975  findsg 3980  funimass2 4492  cofunexg 4501  cofunex2g 4502  fnex 4535  dmfexOLD 4599  dff1o2 4639  resdif 4659  funbrfv 4709  eqfnfv 4766  fvimacnvi 4777  fvimacnvALT 4782  funiunfv 4842  isofrlem 4878  fnotoprb 4916  foprrn 4965  fnoprvrn 4968  tfrlem8 5126  tfrlem9 5127  tfrlem11 5129  tfr3 5134  oasuc 5208  omsuc 5210  oalim 5212  omlim 5213  oalimcl 5242  oaass 5243  omlimcl 5257  odi 5258  omass 5259  oneo 5260  oelim2 5270  oeoelem 5273  nnaordex 5306  nnawordex 5307  oaabslem 5308  ecoprass 5379  ecoprdi 5380  f1oen2g 5453  f1oeng 5454  domentr 5480  undom 5497  ac6sfilem3 5508  ac6sfi 5509  pwuninel 5550  riotaxfrd 5581  mapunen 5596  ssenen 5598  phplem3 5604  phplem4 5605  php 5607  php3 5609  onomeneq 5612  omsucdom 5616  ssfi 5630  unbnn2 5638  unfi 5644  unifi 5648  fodomfi 5656  iunfi 5659  pm54.43 5662  supmaxlem 5678  ordtypelem5 5688  ordtypelem6 5689  omex 5733  omsubsdomlem2 5880  omsubel 5883  elomsubsd 5885  aceq3 5895  aceq5 5902  aceq6b 5904  ac5b 5915  zorn2lem3 5952  imadomg 5968  sucdom 5994  ondomon 6008  alephnbtwn 6016  alephordi 6022  alephval2 6050  cfom 6064  axrepndlem2 6097  axpowndlem4 6104  axinfndlem1 6109  axacndlem5 6115  addclpi 6172  addasspi 6175  mulasspi 6177  distrpi 6178  mulcanpi 6179  indpi 6186  ltapq 6228  ltrpq 6237  prcdpq 6249  genpass 6264  distrlem1pr 6279  distrlem2pr 6280  distrlem4pr 6282  psslinpr 6287  prlem934b 6290  ltexprlem6 6299  ltexprlem7 6300  prlem936b 6306  prlem936 6307  reclem3pr 6310  reclem4pr 6311  recexsrlem 6364  suppsr3 6376  pre-axsup 6444  add4 6491  cnegexlem1 6499  cnegexlem3 6501  cnegex 6502  addsub 6542  subneg 6554  subdi 6590  1re 6598  resubcl 6601  mulneg2 6616  mul2neg 6618  negsubdi 6622  submul2 6625  subsub2 6626  nnncan1OLD 6633  addsub4 6640  xrre 6744  le2tri3i 6764  ltaddsub 6814  leaddsub 6816  lenegcon2 6848  recextlem1 6874  recextlem2 6875  recex 6876  div12 6927  divneg 6950  letrp1 6994  lt2mul2div 7054  lerec2 7072  ledivdiv 7073  ltdiv23 7075  lediv23 7076  lediv12a 7079  ledivp1 7088  nndivre 7135  nndiv 7143  nndivtr 7144  rerpdivcl 7251  lble 7256  sup2 7260  dfinfmr 7276  nnunb 7279  arch 7280  bndndx 7282  xrsupsslem 7285  xrinfmsslem 7286  supxrunb1 7298  nn0addcl 7329  nn0leltp1 7337  nn0addge1 7339  nn0addge2 7340  zaddcl 7374  zsubcl 7377  zrevaddcl 7379  elnn0nn 7380  zltp1le 7390  zleltp1 7391  zltlem1 7393  zdiv 7397  peano2uz2 7413  uzind 7417  uzindOLD 7420  uzwo4OLD 7422  uzwo3lem1 7429  zmax 7433  zbtwnre 7434  rebtwnz 7435  qaddcl 7449  qsubcl 7452  qreccl 7453  qdivcl 7454  qrevaddcl 7455  irradd 7457  irrmul 7458  qbtwnre 7459  qsqueeze 7461  flge 7472  flwordi 7477  flbi 7480  fladdz 7484  modid 7512  modcyc 7516  modcyc2 7517  modmul1 7519  elioc2 7558  elico2 7559  elicc2 7560  icounlem 7581  eluzp1l 7603  uzwo 7624  uzwoOLD 7625  infmssuzle 7634  fzss2 7676  fzsuc 7678  fzrev2 7690  fzrev3i 7693  fzrevral 7698  fsequb 7702  fsequb2 7703  fseqsupubi 7705  seq1rn2 7734  ser1recli 7744  seqzp1 7791  seqzval2 7796  seqzeq 7798  seqzrn2 7799  seqzrn 7800  ser0cl1i 7807  expnnval 7815  expp1 7817  expm1t 7826  expeq0 7828  expge0 7833  expgt1 7834  expge1 7835  bernneq 7898  bernneqOLD 7899  expnlbnd 7902  expnlbnd2 7903  digit1 7905  replim 8011  mulre 8027  resub 8056  imsub 8059  cjsub 8066  sqabsadd 8099  sqabssub 8100  seq1bndi 8162  cau3iri 8167  cau5ii 8169  cvg2i 8174  faccl 8192  facdiv 8194  faclbnd4lem3 8202  faclbnd4lem4 8203  faclbnd5 8205  bccmpl 8214  fsum1s 8269  fsump1s 8273  fsum1ps 8278  fsumsplit 8280  fsumadd 8282  fsumcom 8288  fsumrev 8289  fsumshft 8291  fsummulc1 8293  fsummulc2 8294  fsum2mul 8297  fsumconst 8298  fsumcmp 8300  fsumcmp0 8301  fsumcmpndx2 8302  fsumabs 8303  fsumabs2mul 8304  serzcl2 8309  serzcmp0 8315  binomlem1 8326  binomlem2 8327  binomlem5 8330  clm4i 8340  clm4lei 8341  clm4fi 8342  clm4a 8350  climfnn 8352  2climnn 8362  2climnn0 8363  iserzshft2i 8367  climge0 8372  climaddlem3 8376  climaddc1 8378  climmullem3 8382  climmullem5 8384  climmullem8 8387  climmulc2 8389  climsubc2 8391  clim2serz 8394  iserzmulc1 8396  iserzcmp 8402  clim2serzi 8405  climserzlei 8407  climsupi 8415  caucvglem6 8422  isumrecl 8471  expcnv 8494  explecnv 8495  geoisum1c 8507  cvgratlem1ALT 8509  cvgratlem2ALT 8510  cvgratlem1 8512  cvgratlem2 8513  cvgratlem4 8515  cvgratlem5 8516  fsum0diaglem2 8519  fsum0diag 8520  fsum0diag2 8521  mulc1cncf 8541  ivthlem7 8549  efaddlem5 8604  efaddlem6 8605  efsub 8633  efexp 8634  reeftlcl 8642  sinsub 8720  cossub 8721  demoivreALT 8753  acdc4lem1 8756  acdc5lem1 8760  acdcALT 8765  znnenlem 8770  unbenlem 8773  ruclem13 8791  infxpidmlem1 8821  infxpidmlem8 8828  infxpidmlem11 8831  infxpidmlem12 8832  infdif 8837  iunopn 8868  istps3 8877  eltg 8888  eltg2 8889  tgcl 8894  tgval3 8895  basgen2 8909  bastop1 8912  subbas2 8915  fctop 8920  clsval2 8961  ntrss 8964  isnei 8994  isneip 8996  neips 9003  islp2 9023  iscncl 9047  metreslem 9099  blin 9129  blss 9130  isopn4 9139  opnin 9146  metequiv 9158  metcnpi3 9170  metcnpi4 9171  metcni2 9173  metcnss 9176  metcnss2 9177  lmbr 9206  lmnn 9213  lmuni 9229  causs 9233  lmfexlem2 9235  metelcls 9243  metcnp4 9248  xplmi2 9252  opr1cn 9256  lmcau 9274  bcthlem1 9277  bcthlem9 9285  bcthlem10 9286  bcthlem14 9290  bcthlem16 9292  bcthlem21 9297  grpidinvlem1 9328  grpidinvlem2 9329  grpideu 9333  gxadd 9398  gxnn0mul 9400  resgrprn 9403  grplactfval 9404  ablnncan 9420  issubgi 9431  ablmul 9439  ghgrpilem4 9444  isvc 9532  isnv 9563  nvmul0or 9604  imsmetlem 9655  nvcni3 9663  nvlmle 9665  vacnlem3 9669  nmcnilem 9676  sm1cnilem 9686  ipcl 9704  ip1cnilem2 9713  ip1cnilem3 9714  ip1cnilem5 9716  ip1cnilem6 9717  sspival 9736  lnocoi 9757  nmosetre 9766  nmoge0 9769  nmoub3i 9775  nmobndi 9777  nmlno0lem 9793  blo3i 9802  blometi 9803  blocnilem 9804  cnph 9819  ipasslem2 9832  ipasslem5 9835  ipdi 9844  ipsubdi 9850  ipblnfi 9857  ajmoi 9860  ubthlem3 9874  ubthlem5 9876  ubthlem6 9877  ubthlem7 9878  ubthlem10 9881  ubthlem11 9882  minveclem24 9913  minveclem25 9914  minveclem28 9917  htthlem8 9974  htthlem9 9975  sinper 10039  cosper 10040  abssinper 10062  efifolem7 10082  efif1lem5 10088  efper 10101  axgroth3 10138  dif1en 10172  indexfi 10174  fipreima 10175  symggrpi 10205  uptx 10226  txcn 10227  subtopmetlem 10255  fbssint 10279  fsubbas 10281  extbas1 10291  limfil 10297  hausfillim 10303  filmapf 10307  isfilmap 10308  fmf 10310  fmbas 10311  elfilmap 10312  elfilmap3 10314  flimopn 10321  cncomp 10331  hvsubopr 10517  hvsubcl 10519  hvaddsubval 10534  hvpncan 10540  hvaddeq0 10568  hvmulcan 10571  hvmulcanOLD 10572  his5 10586  his7 10589  his2sub2 10592  hlimcauii 10739  hhssnv 10767  shorth 10801  occllem6 10811  projlem25 10843  projlem26 10844  pjval 10872  pjeq2 10874  chsscon2 11058  chpsscon2 11061  chdmm3 11083  chdmm4 11084  chdmj3 11087  chdmj4 11088  chj4 11091  spansnmul 11120  cmcm2 11192  fh1 11194  fh2 11195  cm2j 11196  spansnscl 11228  spansncvi 11232  5oalem4 11237  homulcl 11322  homco1 11364  homulass 11365  hoadddi 11366  hosubneg 11370  honegsubdi 11373  hosubsub2 11375  hosub4 11376  adjmo 11395  adjsym 11396  cnvadj 11453  nmopub2tALT 11470  unoplin 11481  counop 11482  nmfnleub2 11487  hmoplin 11503  braadd 11506  bramul 11507  kbmul 11516  lnopmul 11528  lnopaddmuli 11534  lnopsubmuli 11536  homco2 11538  nmlnop0iALT 11557  lnopmi 11562  lnophsi 11563  lnopeq0i 11569  unopbd 11577  hmopd 11584  nmophmi 11598  lnopconi 11600  lnfnmuli 11610  lnfnaddmuli 11611  lnfnconi 11627  nlelshi 11630  riesz3i 11632  cnlnadjlem6 11642  adjlnop 11656  adjmul 11662  adjcoi 11670  cnvbramul 11686  leopnmid 11709  hmopidmpji 11724  pjadjcoi 11733  pjss1coi 11735  pjnormssi 11740  pjclem4 11772  pjadj2coi 11777  pj3si 11780  pj3i 11781  hstnmoc 11795  hstle1 11798  hst1h 11799  hstle 11802  hstoh 11804  spansncv2 11865  dmdmd 11872  mdslmd1lem2 11898  mdslmd2i 11902  atcveq0 11920  chcv1 11927  chcv2 11928  cvexchlem 11940  cvp 11947  atcv1 11952  atexch 11953  atomli 11954  atcvatlem 11957  irredlem2 11963  irredi 11966  atdmd 11970  atmd2 11972  mdsymlem3 11977  mdsymlem5 11979  atdmd2 11986  sumdmdlem 11990  sumdmdlem2 11991  cdj1i 12005  cdj3lem1 12006  cdj3lem2b 12009  cdj3i 12013  bnj50OLD 12425  bnj560 12540  bnj588 12554  bnj1126 12932  bnj518 13260  bnj522 13261  bnj535 13265  bnj594 13300  bnj953 13343  bnj1128 13428  bnj1145 13431  elfzm11 13604  elfzp1b 13605  fseq1cl 13619  cayleylem2 13642  ublbneg 13653  nn0seqcvgd 13659  0dvds 13675  dvdssub 13690  dvdslelem 13692  dvdsle 13693  dvdsleabs 13694  divalgb 13707  divalg2 13708  ndvdsadd 13711  gcdcllem1 13718  gcdneg 13732  modgcd 13738  algrf 13739  algrp1lem 13741  mulgcdlem2 13757  mulgcdlem3 13758  dvdsgcd 13765  isprm2lem 13774  isprm3 13776  dfon2lem5 13853  trcltr 13936  poseq 13954  soseq 13955  wfrlem15 13971  sltval2 13997  axfelem14 14044  altxpexg 14101  11st22nd 14348  domrancur1clem 14549  indpre 14580  fprod1s 14677  fprodp1s 14682  reacomsmgrp3 14705  resgcom 14712  mvecrtol2 14820  cbci 14852  subtopsin2 14907  cnfilca 14927  topunfincomp 14957  singcon 14968  iint 15012  issubcat 15193  pwtsm 15266  subtsm 15267  finminlem 15367  elfiun 15369  ordtypelem5OLD 15379  ordtypelem6OLD 15380  omsubsdomlem2OLD 15389  omsubelOLD 15392  elomsubsdOLD 15394  subntr 15425  cnsubsp2 15427  compsub 15431  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem3 15439  alexsub 15441  reconnlem5 15450  reconn 15451  neibastop1 15518  topjoin 15527  ufprim 15569  ufileu 15573  neiplim 15586  limfilcf 15587  flimcls 15588  cnpfillim 15589  fmfnfmlem4 15597  fmfnfm 15598  isfclus 15606  fcluscomp 15621  sfclusf 15624  filnetlem3 15642  unirep 15664  cover2 15673  cocanfo 15689  f1ocan1fv 15717  f1elima 15719  enf1f1o 15720  upixp 15729  eropreu 15733  indexfiOLD 15755  fipreimaOLD 15756  zornn0 15764  infmrgelb 15766  frfi 15771  pofun 15772  filbcmb 15776  addsubeq4 15778  fzsplit 15792  fzm1 15796  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  seqpo 15814  incsequz 15815  incsequz2 15816  fsum00 15820  fsumlt 15821  fsumlt1 15831  unopn 15835  subspopn 15837  subspabs 15840  neificl 15841  lpss2 15842  blhalf 15846  mettrifi 15847  mettrifi2 15848  geomcau 15849  lmclim2 15850  caushft 15851  iccdil 15861  lincmb01cmp 15878  lincmb01icc 15879  cnimass 15888  cnres 15889  cnresima 15891  cnss 15892  hmeocnv 15898  lmtlm 15908  txsubsp 15912  txmet 15925  sstotbnd 15936  totbndss 15937  isbnd3 15941  totbndbnd 15944  ismtyhmeolem 15950  ismtyhmeo 15951  ismtyres 15954  heiborlem1 15955  heiborlem11 15965  heiborlem13 15967  heiborlem15 15969  heiborlem16 15970  heiborlem23 15977  heiborlem29 15983  heiborlem30 15984  heiborlem32 15986  heiborlem33 15987  heiborlem36 15990  heiborlem37 15991  heiborlem42 15996  rrndstprj2 16018  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  exidreslem 16030  ghomco 16040  grpkerinj 16042  phtpycom 16050  phtpycolem1 16051  phtpycolem2 16052  phtpyco 16056  reparpht 16065  pcoval2 16075  pcoloopf 16079  pcohtpy 16083  pcorev 16087  pi1f 16093  pi1val 16094  pi1gp 16095  isdivrng2 16111  isdivrng3 16112  rngisocnv 16135  isfld2 16153  isidlc 16163  idlnegcl 16170  divrngidl 16176  intidl 16177  inidl 16178  unichnidl 16179  maxidlmax 16191  igenmin 16212  isfldidl 16216  erex 16262  smoge 16454  strdif 16719  posref 16775  posgeref 16796  joinval2 16816  meetval2 16823  glbconx 17029  grpidinvlem1NEW 17109  grpidinvlem2NEW 17110  grpideuNEW 17114  psubspi2 17229  linepsub 17232  pmapat 17243  pmap1 17247  polat 17341

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain