Theorem sylan 497

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 402	. . 3 |- (ph -> (ps -> ch))
4	1, 3	syl 12	. 2 |- (th -> (ps -> ch))
5	4	imp 377	1 |- ((th /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  sylanb 498  sylanbr 499  syl2an 503  sylanl1 509  sylanl2 510  syl3an1 1130  syl3anl 1148  eupick 1834  vtocl2gf 2348  csbnest1g 2582  reuss2 2870  sonr 3610  sotr 3611  so2nr 3613  so3nr 3614  wecmpep 3650  wetrep 3651  wereu 3654  ordelss 3674  ordelord 3680  onelon 3683  ordtri3or 3691  ordtri3orOLD 3692  ordsssuc 3756  onmindif 3760  ordunisssuc 3772  ordsucss 3899  ordsucelsucOLD 3903  ordunisuc2 3926  limsssuc 3934  ordomOLD 3961  limom 3967  nnsuc 3969  imadif 4493  fnbr 4515  fnexALT 4536  feu 4588  fex 4595  dffo2 4621  foco 4628  f1dmex 4664  ffoss 4665  nfunsnOLD 4707  funbrfv 4709  fvco 4736  fvopabg 4748  fvimacnvALT 4782  ffvelrn 4787  dffo4 4793  fopabco 4805  fsn2 4809  fvconst2g 4820  funfvima 4828  funiunfv 4842  f1ocnvfv1 4854  f1ocnvfv2 4855  f1ofveu 4858  f1ocnvfv3 4859  f1ocnvdm 4860  isocnv 4873  isotr 4874  isotrALT 4875  isomin 4876  isoini 4877  isowe 4880  f1oiso 4881  curry1f 5076  curry2f 5079  iinon 5115  onfununi 5116  tfrlem2 5120  tfrlem8 5126  tfrlem11 5129  tz7.48lem 5164  oalimcl 5242  oaass 5243  omordi 5245  omword2 5253  omlimcl 5257  odi 5258  omass 5259  oen0 5261  oeordsuc 5269  oelim2 5270  oeoalem 5271  oeoelem 5273  nnaordex 5306  nnawordex 5307  oaabs 5309  ecoprass 5379  f1domg 5455  endomtr 5479  fundmen 5487  pw2en 5505  ac6sfi 5509  sdomdomtr 5532  mapenlem1 5583  mapenlem2 5584  mapxpen 5589  xpmapenlem4 5593  mapunen 5596  ssenen 5598  phplem1 5602  omsucdom 5616  sucdomi 5617  pssnn 5628  ssfi 5630  isfinite2 5639  unfilem1 5641  unifi 5648  suppr 5680  supsnALT 5682  ordiso 5683  ordtypelem6 5689  hartog 5693  r1ord 5766  r1val1 5769  rankr1 5785  r1pwcl 5798  rankxplim3 5825  karden 5856  omsubsdomlem2 5880  infenomsub 5889  ac6lem 5916  ondomon 6008  ondomcard 6009  alephordi 6022  cardaleph 6033  carduniima 6038  cardinfima 6039  cflim 6057  addclpi 6172  addasspi 6175  mulasspi 6177  addnidpi 6180  ltexpq 6232  prub 6250  genpnnp 6260  genpass 6264  addclprlem1 6270  mulclprlem 6273  1idpr 6285  prlem934b 6290  prlem934 6291  ltexprlem4 6297  ltexprlem6 6299  ltexprlem7 6300  reclem3pr 6310  suplem2pr 6314  00sr 6360  mulgt0sr 6366  recexsr 6368  map2psrpr 6372  suppsr 6374  supsrlem6 6382  supre 6412  adddir 6472  add4OLD 6492  cnegexlem3 6501  addsubass 6541  addsub12 6545  2addsub 6548  negcon1 6570  mul4 6581  muladd 6582  muladd11 6584  subdir 6591  negdi2 6621  negsubdi2 6623  neg2sub 6624  subsub4 6629  subadd4 6642  axsup 6676  eqle 6746  le2tri3i 6764  ltaddsub 6814  leaddsub 6816  ltnegcon1 6845  lenegcon1 6847  recex 6876  div12 6927  p1le 6995  ltmul2 7009  ltmul2OLD 7010  gt0div 7035  ge0div 7036  ltdivmulOLD 7050  ledivmulOLD 7052  ltrec1 7071  lerec2 7072  nn2ge 7125  nnltp1le 7139  suprleub 7268  nnunb 7279  xrsupsslem 7285  xrinfmsslem 7286  supxr2 7291  supxrre 7292  supxrunb1 7298  supxrbnd 7300  supxrleub 7308  nn0addcl 7329  elnnz1 7364  zaddcl 7374  elnnnn0b 7382  elnnnn0c 7383  zltp1le 7390  zlem1lt 7392  gtndiv 7405  prime 7407  msqznn 7408  uzindOLD 7420  btwnz 7428  zmax 7433  zbtwnre 7434  rebtwnz 7435  qaddcl 7449  qreccl 7453  qbtwnre 7459  fllt 7473  flbi2 7481  fladdz 7484  ceile 7491  quoremnn0ALT 7493  fldiv 7497  fldiv2 7498  modmulnn 7510  zmodcl 7511  moddi 7520  modsubdir 7521  elioc2 7558  elico2 7559  elicc2 7560  iccsupr 7567  uzss 7600  uzwo2 7626  elfz5 7644  fzss1 7675  fzsuc 7678  fzssp1 7679  fzp1ss 7680  fsequb 7702  fseqsupubi 7705  seq1rn 7735  seq1cl 7738  seq1cl2 7739  ser1addi 7752  shftres 7757  shftval4 7762  shftcan1 7767  seqzfveq 7797  expgt0 7831  expgt1 7834  mulexp 7836  exprec 7837  exprecOLD 7838  expmul 7840  expordi 7845  expmwordi 7851  exple1 7852  expubnd 7853  bernneq 7898  bernneqOLD 7899  expnbnd 7901  digit2 7904  digit1 7905  mulre 8027  cjexp 8067  absnid 8114  absexp 8119  abssubne0 8134  absdiflt 8135  absdifle 8136  lenegsq 8137  seq1bndi 8162  seq1ublem 8163  cau3iri 8167  cau5ii 8169  cvg3i 8175  cvganz 8176  facdiv 8194  facndiv 8195  faclbnd3 8199  faclbnd5 8205  faclbnd6 8206  bccmpl 8214  bccl2 8223  fsump1s 8273  fsumcllem 8274  fsum1ps 8278  fsumsplit 8280  fsumcom 8288  fsumrev 8289  fsumrev2 8290  fsumshftm 8292  fsummulc1 8293  fsumconst 8298  fsumcmpndx2 8302  fsumabs 8303  serz1p 8312  binomlem1 8326  bcxmas 8336  clm3i 8339  climrecl 8370  climge0 8372  climaddlem3 8376  climaddc2 8379  climmullem4 8383  climmullem5 8384  climmullem8 8387  clim2serz 8394  climcmpc1 8399  clim2serzi 8405  climabslem 8408  climsupi 8415  caucvglem2 8418  caucvglem5 8421  caucvglem6 8422  serzf0i 8429  ser1cmp2i 8437  isum1p 8467  expcnv 8494  explecnv 8495  geoisumr 8505  cvgratlem2ALT 8510  cvgratlem5 8516  fsum0diaglem2 8519  fsum0diag2 8521  fsum0diag4 8523  cncffvrn 8535  mulc1cncf 8541  ivthlem7 8549  efexp 8634  eftlcl 8641  reeftlcl 8642  abspef01tlubi 8660  reeff1o 8691  cos01gt0 8743  demoivre 8752  demoivreALT 8753  ruclem13 8791  infxpidmlem1 8821  infxpidmlem7 8827  infxpidmlem10 8830  infxpidmlem11 8831  infxpidmlem12 8832  infcda 8836  infdif 8837  infmap2lem2 8849  tgss2 8907  subtop 8916  iscld 8945  clsval 8953  clsval2 8961  clsndisj 8982  neival 8993  ssnei2 9006  opnneiss 9008  lpval 9019  cnco 9045  cnpco 9046  cncnplem4 9054  sncld 9064  metreslem 9099  metxp 9111  bl2in 9120  blssex 9131  ssblex 9133  opni3 9143  opnin 9146  lpbl 9157  metcnpf 9161  metcnplem 9164  metcnp 9165  metcnss 9176  metcnss2 9177  metidcn 9178  lmbr 9206  lmnn 9213  cmscvg 9225  lmss 9231  causs 9233  lmle 9238  lmclim 9241  metelcls 9243  xplmi 9251  xplm 9253  xpcn 9254  oprcn 9255  opr2cn 9257  iscms2lem4 9270  cmsss 9275  bcthlem16 9292  bcthlem17 9293  bcthlem24 9300  bcthlem25 9301  bcthlem30 9306  bcthlem33 9309  grpidinvlem3 9330  grpidinv 9332  grpidinv2 9344  gxnval 9383  abl23 9412  abl4 9413  ablmuldiv 9415  abldivdiv 9416  abldivdiv4 9417  ablnncan 9420  issubgi 9431  subgabl 9432  ghgrpilem3 9443  ghgrpilem4 9444  gaid 9454  ssga 9455  gacan 9460  gapm 9462  ring2 9474  ringaass 9479  ringa23 9480  ringrcan 9482  ringlcan 9483  ring0rid 9485  ring0lid 9486  vcid 9502  vcaass 9512  vca23 9513  vcrcan 9515  vclcan 9516  vc0rid 9518  vc0lid 9519  vcm 9522  vcrinv 9523  vclinv 9524  vcoprnelem 9529  nvass 9573  nvadd23 9575  nvrcan 9576  nvlcan 9577  nvsid 9580  nvsass 9581  nvdi 9583  nvdir 9584  nv2 9585  nv0rid 9588  nv0lid 9589  nv0 9590  nvsz 9591  nvinv 9592  invfval 9593  nvnnncan1 9600  nvnnncan2 9601  nvnegneg 9603  nvrinv 9605  nvlinv 9606  nvaddsubass 9610  nvaddsub 9611  nvcl 9619  nvmtri2 9632  nvelbl 9657  nvelbl2 9658  nvcnpf 9660  nvlmcl 9664  vacnlem3 9669  vacnlem5 9671  ipid 9702  sspg 9726  ssps 9728  sspmval 9731  sspn 9734  sspival 9736  sspimsval 9738  lnoadd 9758  lnosub 9759  lnomul 9760  nvcnpi3 9761  nvcnpi4 9762  nmoub3i 9775  nmounbi 9778  blometi 9803  ipasslem1 9831  ipasslem2 9832  ipasslem3 9833  ipasslem4 9834  ipasslem5 9835  ipasslem8 9838  ipdi 9844  ipassr 9847  ipsubdir 9849  ipsubdi 9850  sspph 9856  ajval 9863  bnsscmcl 9870  ubthlem3 9874  ubthlem5 9876  ubthlem6 9877  ubthlem9 9880  ubthlem10 9881  ubthlem11 9882  minveclem9 9898  minveclem25 9914  minveclem27 9916  minveclem28 9917  minveclem38 9927  hlass 9950  hladdid 9952  hlmulid 9954  hlmulass 9955  hldi 9956  hldir 9957  hlmul0 9958  hlipdir 9961  hlipass 9962  hlcompl 9964  htthlem5 9971  htthlem6 9972  htthlem8 9974  htthlem10 9976  pstr 9995  spwpr4c 10009  abssinper 10062  efif1lem5 10088  shftefif1olem 10095  explog 10126  reexplog 10127  relogexp 10128  axgroth3 10138  elpreima 10161  dif1en 10172  dif1enOLD 10173  findcard 10178  symggrpi 10205  uptx 10226  txcn 10227  2txcn 10229  elsubsp 10248  subcld 10254  subtopmetlem 10255  subtopmet 10256  fbssint 10279  filrn 10293  limfil 10297  filmapss 10309  elfilmap3 10314  fbaslim 10322  isflimf 10323  cncomp 10331  dirtr 10356  cmpidelt 10376  h2hlm 10482  hvadd4 10537  hvaddsubass 10542  hvmulcan2 10573  hiassdi 10590  hcau2 10688  hlim2 10693  hhcms 10705  hsn0elch 10753  norm1exi 10755  hhssnv 10767  hhsscms 10783  ocsh 10789  occllem6 10811  projlem21 10839  projlem25 10843  projlem26 10844  pjpjth 10891  pjop 10893  pjpo 10894  pjoccl 10899  shsel3 10912  elspancl 10938  chsscon1 11057  chpsscon1 11060  chdmm2 11082  chdmj2 11086  h1de2ctlem 11111  elspansncl 11121  pjspansn 11133  fh2 11195  cm2j 11196  osumlem1 11213  osumlem2 11214  spansncvi 11232  5oalem2 11235  3oalem1 11242  pjo 11251  pjjsi 11280  pjdsi 11292  pjds3i 11293  pjoi0 11297  hoadd4 11347  homco1 11364  homulass 11365  hoadddi 11366  hoadddir 11367  honegsubdi2 11374  hosubadd4 11377  hoaddsubass 11378  hosubsub4 11381  adjsym 11396  cnvadj 11453  hhlnoi 11463  unopf1o 11477  unopnorm 11478  cnvunop 11479  unopadj 11480  unoplin 11481  counop 11482  hmopre 11484  adjcl 11493  adj2 11495  hmoplin 11503  bracl 11510  kbop 11514  kbmul 11516  eighmre 11524  eighmorth 11525  lnopmul 11528  lnopmulsubi 11537  0lnfn 11546  lnopmi 11562  lnophsi 11563  lnopcoi 11565  nmopun 11576  hmops 11582  hmopm 11583  hmopco 11585  nmcopexlem3 11590  nmcopexlem5 11592  nmcopexlem6 11593  lnopconi 11600  nmcfnexlem3 11619  nmcfnexlem5 11621  nmcfnexlem6 11622  lnfnconi 11627  nlelchi 11631  riesz3i 11632  cnlnadjlem2 11638  cnlnadjlem6 11642  cnlnadjlem7 11643  cnlnadjeui 11647  adjbdln 11653  adjlnop 11656  adjmul 11662  adjadd 11663  nmopcoi 11665  adjcoi 11670  nmopcoadji 11671  branmfn 11675  branmfnOLD 11676  cnvbramul 11686  kbass2 11688  kbass5 11691  leop2 11695  leopsq 11700  leopadd 11703  leopmuli 11704  leopmul 11705  leopnmid 11709  nmopleid 11710  pjnmopi 11719  hmopidmchlem 11722  hmopidmchi 11723  pjadjcoi 11733  pjimai 11748  pjadj2coi 11777  stcl 11788  hstcl 11789  staddi 11818  strlem3 11825  strlem4 11826  strlem5 11827  hstrlem3 11833  hstrlem4 11834  hstrlem5 11835  cvcon3 11856  mdbr2 11868  dmdmd 11872  dmdbr5 11880  mddmd2 11881  mdsl0 11882  mdsl3 11888  mdslmd1lem1 11897  mdslmd4i 11905  atsseq 11919  atcveq0 11920  ch1dle 11924  atom1d 11925  superpos 11926  shatomici 11930  shatomistici 11933  cvexchlem 11940  atnem0 11949  atcv0eq 11951  atordi 11956  atcvatlem 11957  irredlem1 11962  irredlem2 11963  irredlem3 11964  atcvat3i 11968  atdmd 11970  mdsymlem5 11979  sumdmdlem 11990  cdj3lem2 12007  bnj48 12422  bnj50 12424  bnj142 12474  bnj214 12508  bnj559 12539  bnj922 12834  bnj948 12847  bnj1072 12902  bnj97 13220  bnj548 13274  bnj900 13325  bnj1145 13431  bnj1498 13562  fseq1cl 13619  cayleylem2 13642  ublbneg 13653  suprzcl 13658  nn0seqcvgd 13659  dvds1lem 13666  dvds2lem 13667  dvdslelem 13692  divalglem8 13703  ndvdsadd 13711  gcdcllem1 13718  gcdcllem3 13720  neggcd 13733  gcdabs 13737  algrp1 13742  alginv 13743  algcvg 13744  algcvga 13747  algfx 13748  eucalgf 13751  eucalgcvga 13754  mulgcdlem2 13757  mulgcdlem7 13762  isprm3 13776  coprm 13782  dfon2lem3 13851  frxp 13951  soseq 13955  wfrlem10 13966  wfrlem14 13970  axdenselem5 14023  axdenselem7 14025  axdenselem8 14026  nocvxminlem 14028  axfelem12 14042  axfelem15 14045  imresord 14427  ordsuccl 14430  ordsuccl2 14431  surjsec2 14467  cbicplem 14508  pre1befi2 14572  supaub 14615  suplub2 14616  nfwpr4c 14630  toplat 14638  fprodp1s 14682  reacomsmgrp1 14703  reacomsmgrp2 14704  clfsebs 14707  addnull1 14806  vwit 14814  muldisc 14824  svs3 14830  truni3 14851  usptoplem 14917  trhom 14983  idmoa 15078  rcmob 15096  dmrngcmp 15098  idosc 15116  dmo 15123  cdmo 15124  jdmo 15125  dualcat2 15133  idsubfun 15206  subtareqbe 15268  ordisoOLD 15374  ordtypelem6OLD 15380  hartogOLD 15384  omsubsdomlem2OLD 15389  infenomsubOLD 15398  opnbnd 15409  cncls 15419  hmeoclda 15421  hmeocldb 15422  subsubtop 15423  compsublem 15430  compsub 15431  cptclsscpt 15432  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem2 15438  alexsub 15441  reconnlem1 15446  reconnlem5 15450  iccconn 15453  fneint 15486  locfindsc 15515  neibastop1 15518  neibastop2lem4 15522  neibastop3 15524  uffixfr 15575  filcon 15580  limfilcf 15587  flimcls 15588  cnpfillim 15589  rnelfm 15593  fmfnfmlem1 15594  fmfnfmlem4 15597  fclusbas 15610  tailuni 15638  tailfb 15639  syldanl 15649  unirep 15664  cover2 15673  foelrn 15685  f1ocan1fv 15717  f1elima 15719  enf1f1o 15720  upixp 15729  erthdmg 15730  eropreu 15733  eroprv 15734  eroprf 15735  infmrlb 15765  frfi 15771  filbcmb 15776  addsubeq4 15778  fzsplit 15792  negmod0 15801  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  incsequz2 15816  fsum00 15820  iserzshft2 15829  csbrni 15832  metf1o 15843  mettrifi 15847  geomcau 15849  lincmb01icc 15879  oprpiece1res1 15880  oprpiece1res2 15881  cnimass 15888  cnres 15889  cnss 15892  paste 15893  hmeoopn 15899  hmeocld 15900  txmet 15925  sstotbnd 15936  bndss 15942  totbndbnd 15944  ismtyhmeolem 15950  heiborlem10 15964  heiborlem13 15967  heiborlem16 15970  heiborlem18 15972  heiborlem30 15984  heiborlem35 15989  bfplem8 16005  bfplem9 16006  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  exidresid 16032  abl4pnp 16037  ghomco 16040  ghomdiv 16041  grpkerinj 16042  phtpycolem4 16054  phtpycolem5 16055  phtpyco 16056  phtpcer 16062  reparphtlem2 16064  reparpht 16065  pcohtpylem1 16080  pcohtpylem2 16081  pcohtpylem3 16082  pcohtpy 16083  pcoass 16085  pcorevlem 16086  pcorev 16087  ringnegcl 16098  ringaddneg1 16099  ringaddneg2 16100  isdivrng2 16111  rnghomcl 16121  rnghomadd 16123  rnghommul 16124  rnghomsub 16127  rnghomco 16128  rngisocnv 16135  iscringd 16147  crngm23 16150  crngm4 16151  idlcl 16165  divrngidl 16176  igenval 16209  igenidl 16211  prnc 16215  isfldidl 16216  pridlc 16219  dmncan1 16224  dmncan2 16225  erex 16262  prtlem11 16268  prter3 16286  ordintdif 16440  smores2 16447  smofvon 16450  smoel 16451  smoiso 16453  latref 16855  lattr 16858  lubub 16895  lubl 16896  olj01 16944  oldmm1 16946  oldmm2 16947  oldmm4 16949  oldmj1 16950  oldmj2 16951  oldmj4 16953  olm0 16958  omllaw2 16965  omllaw3 16966  cmtcomlem 16969  omlfh1 16978  glbconx 17029  hlatmstc 17047  hlatle 17048  cvratlem 17061  ps-1 17078  grpidinvlem3NEW 17111  grpidinvNEW 17113  grpidinv2NEW 17119  invrcl 17171  linepsub 17232  pmapsub 17250  paddssw2 17305  2polpmap 17325  2polat 17342

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