Theorem sylan 448

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sylanb 449  sylanbr 450  syl2an 454  sylanl1 460  sylanl2 461  syl3an1 859  syl3anl 876  eupick 1434  vtocl2gf 1849  csbnest1g 2037  reuss2 2275  sonr 2855  sotr 2856  so2nr 2858  so3nr 2859  wecmpep 2941  wetrep 2942  wereu 2945  ordelss 2964  ordelord 2970  onelon 2972  ordtri3or 2979  ordsssuc 3057  onmindif 3060  ordsucss 3069  ordsucelsuc 3073  ordunisssuc 3083  ordunisuc2 3115  limsssuc 3121  ordom 3141  limom 3146  nnsuc 3148  imadif 3574  fnbr 3590  fnex 3607  feu 3647  fex 3652  dffo2 3675  foco 3682  f1dmex 3710  ffoss 3711  funbrfv 3750  fvco 3774  fvopabg 3785  fvimacnvALT 3809  ffvelrn 3814  dffo4 3820  fopabco 3832  fsn2 3836  fvconst2g 3844  funfvima 3852  funiunfv 3866  f1ocnvfv1 3878  f1ocnvfv2 3879  f1ofveu 3882  f1ocnvfv3 3883  f1ocnvdm 3884  isocnv 3896  isotr 3897  isotrALT 3898  isomin 3899  isoini 3900  isowe 3903  f1oiso 3904  iinon 3910  tfrlem2 3912  tfrlem8 3918  tfrlem11 3921  tz7.48lem 3955  curry1f 4099  oalimcl 4194  oaass 4195  omordi 4197  omword2 4205  omlimcl 4209  odi 4210  omass 4211  oen0 4213  oeordsuc 4221  oelim2 4222  nnaordex 4249  nnawordex 4250  oaabs 4252  ecoprass 4320  mapsn 4345  f1domg 4396  endomtr 4420  fundmen 4428  pw2en 4446  sdomdomtr 4469  mapenlem1 4489  mapenlem2 4490  mapxpen 4495  xpmapenlem4 4499  mapunen 4502  ssenen 4504  phplem1 4508  omsucdom 4523  sucdomi 4524  pssnn 4534  ssfi 4537  ssfiOLD 4538  isfinite2OLD 4546  unfilem1 4548  unifiOLD 4557  fodomfibOLD 4567  suppr 4590  supsnALT 4592  r1ord 4655  r1val1 4658  rankr1 4674  r1pwcl 4687  rankxplim3 4714  karden 4726  ac6lem 4754  ondomon 4856  ondomcard 4857  alephordi 4874  cardaleph 4885  carduniima 4890  cardinfima 4891  cflim 4909  addclpi 5020  addasspi 5023  mulasspi 5025  addnidpi 5028  ltexpq 5080  prub 5098  genpnnp 5108  genpass 5112  addclprlem1 5118  mulclprlem 5121  1idpr 5133  prlem934b 5138  prlem934 5139  ltexprlem4 5145  ltexprlem6 5147  ltexprlem7 5148  reclem3pr 5158  suplem2pr 5162  00sr 5208  mulgt0sr 5214  recexsr 5216  map2psrpr 5220  suppsr 5222  supsrlem6 5230  supre 5260  adddirt 5319  add4t 5338  cnegextlem3 5347  addsubasst 5383  addsub12t 5386  2addsubt 5389  negcon1t 5410  mul4t 5420  muladd11t 5422  subdirt 5428  negdi2t 5456  negsubdi2t 5458  neg2subt 5459  subsub4t 5464  subadd4t 5475  axsup 5507  eqlet 5571  le2tri3 5589  ltaddsubt 5631  leaddsubt 5633  ltnegcon1t 5656  lenegcon1t 5658  recext 5684  divasst 5741  p1let 5817  ltmul2t 5831  gt0divt 5853  ge0divt 5854  ltdivmultOLD 5868  ledivmultOLD 5869  ltrec1t 5888  lerec2t 5889  ltdiv23t 5892  lediv23t 5893  nn2get 5942  nnltp1let 5955  suprleub 6059  nnunb 6070  xrsupsslem 6076  xrinfmsslem 6077  supxr2 6082  supxrre 6083  supxrunb1 6089  supxrbnd 6091  supxrleub 6099  nn0addclt 6120  elnnz1 6155  zaddclt 6165  elnnnn0b 6173  elnnnn0c 6174  zltp1let 6181  zlem1ltt 6183  gtndivt 6193  primet 6195  msqznn 6196  uzindOLD 6208  btwnz 6215  zmax 6220  zbtwnre 6221  rebtwnz 6222  flltt 6234  flbi2t 6241  fladdzt 6244  ceilet 6250  qaddclt 6269  qrecclt 6273  qdivclt 6274  qbtwnre 6278  seq1rn 6322  seq1cl 6325  seq1cl2 6326  ser1add 6339  shftres 6344  shftval4t 6349  shftcan1t 6354  elioc2t 6390  elico2t 6391  elicc2t 6392  iccsupr 6398  uzss 6431  uzwo2 6457  elfz5t 6474  fzss1t 6503  fzssp1t 6506  fzp1sst 6507  fsequb 6523  fseqsupub 6526  seqzfveq 6554  expgt0t 6589  expgt1t 6592  mulexpt 6594  recexpt 6595  expmult 6597  expordit 6600  expmwordit 6606  exple1t 6607  expubndt 6608  bernneq 6652  expnbndt 6654  sqrlem5 6677  mulretOLD 6777  cjexpt 6817  absnidt 6863  absexpt 6868  abssubne0t 6882  absdifltt 6883  absdiflet 6884  lenegsqt 6885  seq1bnd 6910  seq1ublem 6911  cau3ir 6915  cau5i 6917  cvg3 6923  cvganz 6924  facdivt 6942  facndivt 6943  faclbnd3 6947  faclbnd5 6953  faclbnd6 6954  bccmplt 6962  bccl2t 6971  fsump1s 7013  fsumcllem 7014  fsum1ps 7018  fsumsplit 7020  fsumcom 7028  fsumrev 7029  fsumrev2 7030  fsumshftm 7032  fsummulc1 7033  fsumconst 7038  fsumcmpndx2 7042  fsumabs 7043  serz1p 7052  binomlem1 7066  bcxmas 7076  clm3 7079  climrecl 7110  climge0 7112  climaddlem3 7116  climaddc2 7119  climmullem4 7123  climmullem5 7124  climmullem8 7127  clim2serzt 7134  climcmpc1 7139  clim2serz 7145  climabslem 7148  climsup 7155  caucvglem2 7158  caucvglem5 7161  caucvglem6 7162  serzf0 7169  ser1f0 7170  ser1cmp2 7177  isum1p 7206  expcnv 7233  geoisumr 7243  cvgratlem2ALT 7248  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag2 7259  fsum0diag4 7261  cncffvrn 7273  mulc1cncf 7279  ivthlem7 7287  efexpt 7372  eftlclt 7379  reeftlclt 7380  abspef01tlub 7395  reeff1o 7426  cos01gt0 7477  demoivre 7484  demoivreALT 7485  ruclem13 7522  infxpidmlem1 7552  infxpidmlem7 7558  infxpidmlem10 7561  infxpidmlem11 7562  infxpidmlem12 7563  infcda 7567  infdif 7568  infmap2lem2 7580  tgss2t 7637  subtop 7646  iscld 7669  clsval 7677  clsval2 7685  clsndisj 7706  neival 7717  ssnei2 7730  opnneiss 7732  lpval 7743  cnco 7768  cnpco 7769  cncnplem4 7777  sncld 7787  metreslem 7822  metxp 7834  bl2in 7843  blssex 7854  ssblex 7856  opni3 7866  opnin 7869  lpbl 7880  metcnpf 7883  metcnplem 7886  metcnp 7887  metcnss 7898  metcnss2 7899  metidcn 7900  lmbr 7928  lmnn 7935  cmscvg 7947  lmss 7953  causs 7955  lmle 7960  lmclim 7963  metelcls 7965  xplmi 7973  xplm 7975  xpcn 7976  oprcn 7977  opr2cn 7979  iscms2lem4 7992  cmsss 7997  bcthlem16 8014  bcthlem17 8015  bcthlem24 8022  bcthlem25 8023  bcthlem30 8028  bcthlem33 8031  grpidinvlem3 8050  grpidinv 8052  grpidinv2 8060  abl23 8104  abl4 8105  ablmuldiv 8107  abldivdiv 8108  abldivdiv4 8109  ablnncan 8112  issubgi 8122  subgabl 8123  ghgrpilem3 8135  ghgrpilem4 8136  ring2 8149  ringaass 8154  ringa23 8155  ringrcan 8157  ringlcan 8158  ring0rid 8160  ring0lid 8161  vcid 8170  vcaass 8180  vca23 8181  vcrcan 8183  vclcan 8184  vc0rid 8186  vc0lid 8187  vcm 8190  vcrinv 8191  vclinv 8192  vcoprnelem 8197  nvass 8241  nvadd23 8243  nvrcan 8244  nvlcan 8245  nvsid 8248  nvsass 8249  nvdi 8251  nvdir 8252  nv2 8253  nv0rid 8256  nv0lid 8257  nv0 8258  nvsz 8259  nvinv 8260  invfval 8261  nvnnncan1 8268  nvnnncan2 8269  nvnegneg 8271  nvrinv 8273  nvlinv 8274  nvaddsubass 8278  nvaddsub 8279  nvcl 8287  nvmtri2 8300  nvelbl 8325  nvelbl2 8326  nvcnpf 8328  nvlmcl 8332  ipid 8363  sspg 8387  ssps 8389  sspmval 8392  sspn 8395  sspival 8397  sspimsval 8399  lnoadd 8419  lnosub 8420  lnomul 8421  nvcnpi3 8422  nvcnpi4 8423  nmoub3i 8436  nmounbi 8439  blometi 8463  ipasslem1 8490  ipasslem2 8491  ipasslem3 8492  ipasslem4 8493  ipasslem5 8494  ipasslem8 8497  ipdi 8503  ipassr 8506  ipsubdir 8508  ipsubdi 8509  sspph 8515  ubthlem3 8531  ubthlem5 8533  ubthlem6 8534  ubthlem9 8537  ubthlem10 8538  ubthlem11 8539  minveclem9 8553  minveclem25 8569  minveclem27 8571  minveclem28 8572  minveclem38 8582  hlass 8603  hladdid 8605  hlmulid 8607  hlmulass 8608  hldi 8609  hldir 8610  hlmul0 8611  hlipdir 8614  hlipass 8615  hlcompl 8617  htthlem5 8624  htthlem6 8625  htthlem8 8627  htthlem10 8629  pstr 8652  spwpr3OLD 8662  abssinper 8712  efif1lem5 8734  shftefif1olem 8741  explogt 8772  reexplogt 8773  relogexpt 8774  axgroth3 8779  h2hlm 8850  hvadd4t 8905  hvaddsubasst 8910  hvmulcan2t 8940  hiassdit 8957  hcau2 9055  hlim2 9060  hhcms 9072  hsn0elch 9120  norm1ex 9122  hhssnv 9134  hhsscms 9150  ocsh 9156  occllem6 9178  projlem21 9206  projlem25 9210  projlem26 9211  pjpjtht 9258  pjopt 9260  pjpot 9261  pjocclt 9266  shsel3t 9279  elspanclt 9305  chsscon1t 9424  chpsscon1t 9427  chdmm2t 9449  chdmj2t 9453  h1de2ctlem 9478  elspansnclt 9488  pjspansnt 9500  fh2t 9562  cm2jt 9563  osumlem1 9578  osumlem2 9579  spansncv 9597  5oalem2 9600  3oalem1 9607  pjot 9616  pjjs 9645  pjds 9657  pjds3 9658  pjoi0t 9662  hoadd4t 9710  homco1t 9727  homulasst 9728  hoadddit 9729  hoadddirt 9730  honegsubdi2t 9737  hosubadd4t 9740  hoaddsubasst 9741  hosubsub4t 9744  adjsymt 9759  cnvadj 9816  hhlno 9826  unopf1ot 9840  unopnormt 9841  cnvunopt 9842  unopadjt 9843  unoplint 9844  counopt 9845  hmopret 9847  adjclt 9856  adj2t 9858  hmoplint 9866  braclt 9873  kbopt 9877  kbmult 9879  eighmret 9887  eighmortht 9888  lnopmult 9891  lnopmulsub 9900  0lnfn 9909  lnopm 9925  lnophs 9926  lnopco 9928  nmopunt 9939  hmopst 9945  hmopmt 9946  hmopcot 9948  nmcopexlem3 9953  nmcopexlem5 9955  nmcopexlem6 9956  lnopcon 9963  nmcfnexlem3 9982  nmcfnexlem5 9984  nmcfnexlem6 9985  lnfncon 9990  nlelch 9994  riesz3 9995  cnlnadjlem2 10001  cnlnadjlem6 10005  cnlnadjlem7 10006  cnlnadjeu 10010  adjbdlnt 10016  adjlnopt 10019  adjmult 10025  adjaddt 10026  nmopco 10028  adjco 10033  nmopcoadj 10034  branmfnt 10038  cnvbramult 10048  kbass2t 10050  kbass5t 10053  leop2t 10057  leopsqt 10062  leopaddt 10065  leopmulit 10066  leopmult 10067  leopnmidt 10071  nmopleidt 10072  pjnmop 10075  hmopidmchlem 10078  hmopidmch 10079  pjadjco 10089  pjima 10104  pjadj2co 10132  stclt 10143  hstclt 10144  stadd 10173  strlem3 10180  strlem4 10181  strlem5 10182  hstrlem3 10188  hstrlem4 10189  hstrlem5 10190  cvcon3t 10211  mdbr2 10223  dmdmdt 10227  dmdbr5 10235  mddmd 10236  mdsl0 10237  mdsl3t 10243  mdslmd1lem1 10252  mdslmd4 10260  atsseq 10274  atcveq0 10275  ch1dle 10279  atom1d 10280  superpos 10281  shatomic 10285  shatomistic 10288  cvexchlem 10295  atnem0 10304  atcv0eq 10306  atord 10311  atcvatlem 10312  irredlem1 10317  irredlem2 10318  irredlem3 10319  atcvat3 10323  atdmd 10325  mdsymlem5 10334  sumdmdlem 10345  cdj3lem2 10362  symggrpi 10406  cayleylem2 10410  idmoa 10664  rcmob 10682  idosc 10702  dmo 10709  cdmo 10710  jdmo 10711  homib 10724  iri 10728

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 147  df-an 225

Copyright terms: Public domain