Theorem sylan 450

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylan	|- ((th /\ ps) -> ch)

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.2	. . 3 |- (th -> ph)
2		sylan.1	. . . 4 |- ((ph /\ ps) -> ch)
3	2	ex 371	. . 3 |- (ph -> (ps -> ch))
4	1, 3	syl 10	. 2 |- (th -> (ps -> ch))
5	4	imp 348	1 |- ((th /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  sylanb 451  sylanbr 452  syl2an 456  sylanl1 462  sylanl2 463  syl3an1 865  syl3anl 882  eupick 1473  vtocl2gf 1895  csbnest1g 2089  reuss2 2327  sonr 2934  sotr 2935  so2nr 2937  so3nr 2938  wecmpep 2968  wetrep 2969  wereu 2972  ordelss 2991  ordelord 2997  onelon 3000  ordtri3or 3007  ordsssuc 3058  onmindif 3061  ordunisssuc 3072  ordsucss 3175  ordsucelsuc 3178  ordunisuc2 3198  limsssuc 3204  ordom 3228  limom 3233  nnsuc 3235  imadif 3679  fnbr 3696  fnex 3713  feu 3754  fex 3759  dffo2 3783  foco 3790  f1dmex 3821  ffoss 3822  funbrfv 3861  fvco 3885  fvopabg 3896  fvimacnvALT 3923  ffvelrn 3928  dffo4 3934  fopabco 3946  fsn2 3950  fvconst2g 3958  funfvima 3966  funiunfv 3980  f1ocnvfv1 3992  f1ocnvfv2 3993  f1ofveu 3996  f1ocnvfv3 3997  f1ocnvdm 3998  isocnv 4010  isotr 4011  isotrALT 4012  isomin 4013  isoini 4014  isowe 4017  f1oiso 4018  curry1f 4194  curry2f 4197  iinon 4208  onfununi 4209  tfrlem2 4213  tfrlem8 4219  tfrlem11 4222  tz7.48lem 4256  oalimcl 4330  oaass 4331  omordi 4333  omword2 4341  omlimcl 4345  odi 4346  omass 4347  oen0 4349  oeordsuc 4357  oelim2 4358  oeoalem 4359  oeoelem 4361  nnaordex 4389  nnawordex 4390  oaabs 4392  ecoprass 4461  mapsn 4486  f1domg 4537  endomtr 4561  fundmen 4569  pw2en 4587  ac6sfi 4591  sdomdomtr 4614  mapenlem1 4636  mapenlem2 4637  mapxpen 4642  xpmapenlem4 4646  mapunen 4649  ssenen 4651  phplem1 4655  omsucdom 4669  sucdomi 4670  pssnn 4681  ssfi 4683  isfinite2 4692  unfilem1 4694  unifi 4701  suppr 4733  supsnALT 4735  r1ord 4801  r1val1 4804  rankr1 4820  r1pwcl 4833  rankxplim3 4860  karden 4872  ac6lem 4900  ondomon 5006  ondomcard 5007  alephordi 5024  cardaleph 5035  carduniima 5040  cardinfima 5041  cflim 5059  addclpi 5174  addasspi 5177  mulasspi 5179  addnidpi 5182  ltexpq 5234  prub 5252  genpnnp 5262  genpass 5266  addclprlem1 5272  mulclprlem 5275  1idpr 5287  prlem934b 5292  prlem934 5293  ltexprlem4 5299  ltexprlem6 5301  ltexprlem7 5302  reclem3pr 5312  suplem2pr 5316  00sr 5362  mulgt0sr 5368  recexsr 5370  map2psrpr 5374  suppsr 5376  supsrlem6 5384  supre 5414  adddir 5473  add4 5492  cnegexlem3 5501  addsubass 5537  addsub12 5540  2addsub 5543  negcon1 5564  mul4 5574  muladd11 5576  subdir 5582  negdi2 5610  negsubdi2 5612  neg2sub 5613  subsub4 5618  subadd4 5629  axsup 5661  eqle 5725  le2tri3i 5743  ltaddsub 5785  leaddsub 5787  ltnegcon1 5810  lenegcon1 5812  recex 5840  div12 5890  p1le 5957  ltmul2 5971  ltmul2OLD 5972  gt0div 5997  ge0div 5998  ltdivmulOLD 6012  ledivmulOLD 6014  ltrec1 6033  lerec2 6034  nn2ge 6087  nnltp1le 6101  suprleub 6227  nnunb 6238  xrsupsslem 6244  xrinfmsslem 6245  supxr2 6250  supxrre 6251  supxrunb1 6257  supxrbnd 6259  supxrleub 6267  nn0addcl 6288  elnnz1 6323  zaddcl 6333  elnnnn0b 6341  elnnnn0c 6342  zltp1le 6349  zlem1lt 6351  gtndiv 6364  prime 6366  msqznn 6367  uzindOLD 6379  btwnz 6387  zmax 6392  zbtwnre 6393  rebtwnz 6394  qaddcl 6408  qreccl 6412  qbtwnre 6418  fllt 6432  flbi2 6440  fladdz 6443  ceile 6450  quoremnn0ALT 6452  fldiv 6456  fldiv2 6457  modmulnn 6469  zmodcl 6470  moddi 6479  modsubdir 6480  elioc2 6516  elico2 6517  elicc2 6518  iccsupr 6525  uzss 6558  uzwo2 6584  elfz5 6602  fzss1 6633  fzsuc 6636  fzssp1 6637  fzp1ss 6638  fsequb 6654  fseqsupubi 6657  seq1rn 6687  seq1cl 6690  seq1cl2 6691  ser1addi 6704  shftres 6709  shftval4 6714  shftcan1 6719  seqzfveq 6749  expgt0 6783  expgt1 6786  mulexp 6788  exprec 6789  exprecOLD 6790  expmul 6792  expordi 6797  expmwordi 6803  exple1 6804  expubnd 6805  bernneq 6849  bernneqOLD 6850  expnbnd 6852  digit2 6855  digit1 6856  sqrlem5 6878  mulre 6978  cjexp 7018  absnid 7065  absexp 7070  abssubne0 7085  absdiflt 7086  absdifle 7087  lenegsq 7088  seq1bndi 7113  seq1ublem 7114  cau3iri 7118  cau5ii 7120  cvg3i 7126  cvganz 7127  facdiv 7145  facndiv 7146  faclbnd3 7150  faclbnd5 7156  faclbnd6 7157  bccmpl 7165  bccl2 7174  fsump1s 7216  fsumcllem 7217  fsum1ps 7221  fsumsplit 7223  fsumcom 7231  fsumrev 7232  fsumrev2 7233  fsumshftm 7235  fsummulc1 7236  fsumconst 7241  fsumcmpndx2 7245  fsumabs 7246  serz1p 7255  binomlem1 7269  bcxmas 7279  clm3i 7282  climrecl 7313  climge0 7315  climaddlem3 7319  climaddc2 7322  climmullem4 7326  climmullem5 7327  climmullem8 7330  clim2serz 7337  climcmpc1 7342  clim2serzi 7348  climabslem 7351  climsupi 7358  caucvglem2 7361  caucvglem5 7364  caucvglem6 7365  serzf0i 7372  ser1cmp2i 7380  isum1p 7410  expcnv 7437  explecnv 7438  geoisumr 7448  cvgratlem2ALT 7453  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag2 7464  fsum0diag4 7466  cncffvrn 7478  mulc1cncf 7484  ivthlem7 7492  efexp 7577  eftlcl 7584  reeftlcl 7585  abspef01tlubi 7603  reeff1o 7634  cos01gt0 7686  demoivre 7695  demoivreALT 7696  ruclem13 7734  infxpidmlem1 7764  infxpidmlem7 7770  infxpidmlem10 7773  infxpidmlem11 7774  infxpidmlem12 7775  infcda 7779  infdif 7780  infmap2lem2 7792  tgss2 7849  subtop 7858  iscld 7879  clsval 7887  clsval2 7895  clsndisj 7916  neival 7927  ssnei2 7940  opnneiss 7942  lpval 7953  cnco 7978  cnpco 7979  cncnplem4 7987  sncld 7997  metreslem 8032  metxp 8044  bl2in 8053  blssex 8064  ssblex 8066  opni3 8076  opnin 8079  lpbl 8090  metcnpf 8094  metcnplem 8097  metcnp 8098  metcnss 8109  metcnss2 8110  metidcn 8111  lmbr 8139  lmnn 8146  cmscvg 8158  lmss 8164  causs 8166  lmle 8171  lmclim 8174  metelcls 8176  xplmi 8184  xplm 8186  xpcn 8187  oprcn 8188  opr2cn 8190  iscms2lem4 8203  cmsss 8208  bcthlem16 8225  bcthlem17 8226  bcthlem24 8233  bcthlem25 8234  bcthlem30 8239  bcthlem33 8242  grpidinvlem3 8263  grpidinv 8265  grpidinv2 8277  gxnval 8316  abl23 8345  abl4 8346  ablmuldiv 8348  abldivdiv 8349  abldivdiv4 8350  ablnncan 8353  issubgi 8364  subgabl 8365  ghgrpilem3 8376  ghgrpilem4 8377  ring2 8391  ringaass 8396  ringa23 8397  ringrcan 8399  ringlcan 8400  ring0rid 8402  ring0lid 8403  vcid 8417  vcaass 8427  vca23 8428  vcrcan 8430  vclcan 8431  vc0rid 8433  vc0lid 8434  vcm 8437  vcrinv 8438  vclinv 8439  vcoprnelem 8444  nvass 8488  nvadd23 8490  nvrcan 8491  nvlcan 8492  nvsid 8495  nvsass 8496  nvdi 8498  nvdir 8499  nv2 8500  nv0rid 8503  nv0lid 8504  nv0 8505  nvsz 8506  nvinv 8507  invfval 8508  nvnnncan1 8515  nvnnncan2 8516  nvnegneg 8518  nvrinv 8520  nvlinv 8521  nvaddsubass 8525  nvaddsub 8526  nvcl 8534  nvmtri2 8547  nvelbl 8572  nvelbl2 8573  nvcnpf 8575  nvlmcl 8579  vacnlem3 8584  vacnlem5 8586  ipid 8617  sspg 8641  ssps 8643  sspmval 8646  sspn 8649  sspival 8651  sspimsval 8653  lnoadd 8673  lnosub 8674  lnomul 8675  nvcnpi3 8676  nvcnpi4 8677  nmoub3i 8690  nmounbi 8693  blometi 8718  ipasslem1 8746  ipasslem2 8747  ipasslem3 8748  ipasslem4 8749  ipasslem5 8750  ipasslem8 8753  ipdi 8759  ipassr 8762  ipsubdir 8764  ipsubdi 8765  sspph 8771  ajval 8778  bnsscmcl 8785  ubthlem3 8789  ubthlem5 8791  ubthlem6 8792  ubthlem9 8795  ubthlem10 8796  ubthlem11 8797  minveclem9 8813  minveclem25 8829  minveclem27 8831  minveclem28 8832  minveclem38 8842  hlass 8865  hladdid 8867  hlmulid 8869  hlmulass 8870  hldi 8871  hldir 8872  hlmul0 8873  hlipdir 8876  hlipass 8877  hlcompl 8879  htthlem5 8886  htthlem6 8887  htthlem8 8889  htthlem10 8891  pstr 8914  spwpr4c 8928  abssinper 8980  efif1lem5 9006  shftefif1olem 9013  explog 9044  reexplog 9045  relogexp 9046  axgroth3 9051  h2hlm 9125  hvadd4 9180  hvaddsubass 9185  hvmulcan2 9216  hiassdi 9233  hcau2 9331  hlim2 9336  hhcms 9348  hsn0elch 9396  norm1exi 9398  hhssnv 9410  hhsscms 9426  ocsh 9432  occllem6 9454  projlem21 9482  projlem25 9486  projlem26 9487  pjpjth 9534  pjop 9536  pjpo 9537  pjoccl 9542  shsel3 9555  elspancl 9581  chsscon1 9700  chpsscon1 9703  chdmm2 9725  chdmj2 9729  h1de2ctlem 9754  elspansncl 9764  pjspansn 9776  fh2 9838  cm2j 9839  osumlem1 9856  osumlem2 9857  spansncvi 9875  5oalem2 9878  3oalem1 9885  pjo 9894  pjjsi 9923  pjdsi 9935  pjds3i 9936  pjoi0 9940  hoadd4 9990  homco1 10007  homulass 10008  hoadddi 10009  hoadddir 10010  honegsubdi2 10017  hosubadd4 10020  hoaddsubass 10021  hosubsub4 10024  adjsym 10039  cnvadj 10096  hhlnoi 10106  unopf1o 10120  unopnorm 10121  cnvunop 10122  unopadj 10123  unoplin 10124  counop 10125  hmopre 10127  adjcl 10136  adj2 10138  hmoplin 10146  bracl 10153  kbop 10157  kbmul 10159  eighmre 10167  lnopmul 10170  lnopmulsubi 10179  0lnfn 10188  lnopmi 10204  lnophsi 10205  lnopcoi 10207  nmopun 10218  hmops 10224  hmopm 10225  hmopco 10227  nmcopexlem3 10232  nmcopexlem5 10234  nmcopexlem6 10235  lnopconi 10242  nmcfnexlem3 10261  nmcfnexlem5 10263  nmcfnexlem6 10264  lnfnconi 10269  nlelchi 10273  riesz3i 10274  cnlnadjlem2 10280  cnlnadjlem6 10284  cnlnadjlem7 10285  cnlnadjeui 10289  adjbdln 10295  adjlnop 10298  adjmul 10304  adjadd 10305  nmopcoi 10307  adjcoi 10312  nmopcoadji 10313  branmfn 10317  branmfnOLD 10318  cnvbramul 10328  kbass2 10330  kbass5 10333  leop2 10337  leopsq 10342  leopadd 10345  leopmuli 10346  leopmul 10347  leopnmid 10351  nmopleid 10352  pjnmopi 10355  hmopidmchlem 10358  hmopidmchi 10359  pjadjcoi 10369  pjimai 10384  pjadj2coi 10413  stcl 10424  hstcl 10425  staddi 10454  strlem3 10461  strlem4 10462  strlem5 10463  hstrlem3 10469  hstrlem4 10470  hstrlem5 10471  cvcon3 10492  mdbr2 10504  dmdmd 10508  dmdbr5 10516  mddmd2 10517  mdsl0 10518  mdsl3 10524  mdslmd1lem1 10533  mdslmd4i 10541  atsseq 10555  atcveq0 10556  ch1dle 10560  atom1d 10561  superpos 10562  shatomici 10566  shatomistici 10569  cvexchlem 10576  atnem0 10585  atnem0OLD 10586  atcv0eq 10588  atordi 10593  atcvatlem 10594  irredlem1 10599  irredlem2 10600  irredlem3 10601  atcvat3i 10605  atdmd 10607  mdsymlem5 10616  sumdmdlem 10627  cdj3lem2 10644  symggrpi 10691  cayleylem2 10695  toplat 10884  cmpidelt 10906  truni3 11001  idmoa 11185  rcmob 11203  dmrngcmp 11205  idosc 11223  dmo 11230  cdmo 11231  jdmo 11232  idsubfun 11312  ordiso 11426  ordtypelem6 11432  hartog 11436  omsubsdomlem2 11441  infenomsub 11450  opnbnd 11461  cncls 11473  hmeoclda 11475  hmeocldb 11476  elsubsp 11477  subsubtop 11479  subcld 11480  compsublem 11487  compsub 11488  cptclsscpt 11489  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem2 11497  alexsub 11500  subtopmetlem 11505  subtopmet 11506  reconnlem1 11507  reconnlem5 11511  iccconn 11514  fneint 11547  locfindsc 11576  neibastop1 11579  neibastop2lem4 11583  neibastop3 11585  fbssint 11626  filrn 11643  uffixfr 11660  filcon 11665  limfil 11675  fbaslim 11680  limfilcf 11683  flimcls 11684  cnpfillim 11686  elfilmap3 11692  filmapss 11696  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem4 11703  isflimf 11709  fclusbas 11722  dirtr 11753  tailuni 11761  tailfb 11762  gaid 11776  ssga 11777  gacan 11782  gapm 11784  elpreima 11792  f1ocan1fv 11816  f1elima 11818  upixp 11823  erthdmg 11824  dif1en 11833  filbcmb 11857  negmod0 11872  sdclem1 11875  sdclem2 11876  sdc 11877  incsequz2 11880  fsum00 11883  iserzshft2 11892  csbrni 11895  metf1o 11907  mettrifi 11912  geomcau 11914  lincmb01icc 11943  cnimass 11949  cnres 11950  cnss 11953  paste 11954  hmeoopn 11960  hmeocld 11961  uptx 11978  txcn 11979  2txcn 11982  sstotbnd 11992  bndss 11998  totbndbnd 12000  ismtyhmeolem 12006  heiborlem10 12020  heiborlem13 12023  heiborlem16 12026  heiborlem18 12028  heiborlem30 12040  heiborlem35 12045  bfplem8 12061  bfplem9 12062  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  phtpycolem4 12096  phtpycolem5 12097  phtpyco 12098  phtpcer 12104

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 145  df-an 223

Copyright terms: Public domain